離散数学でtruth tableを使って論理検証する場面がいくつかあったので、その時のためにプログラムを作っておきます。
一般に、要素が1つ増えるごとに組み合わせは２倍になるため再帰を使用して実装した方が良さそうです。
目次
全パターン取得の再帰関数の定義
def r_TT(n:int,s:str,a:int,l:list=[]) -> list:
if n == 0:
return []
else:
if len(s+"T") == a:
l += [s+"T"]
l += [s+"F"]
r_TT(n-1,s+"T",a,l)
r_TT(n-1,s+"F",a,l)
return l
r_TT(3,"",3)
>>>
['TTT', 'TTF', 'TFT', 'TFF', 'FTT', 'FTF', 'FFT', 'FFF']論理式の検証
evalを使用して論理式の検証を行います。
def rep(prop:str) -> str:
return prop.replace(" ","").replace("¬","not ").replace("∧"," and ").replace("∨"," or ")
def leq(prop1, prop2, vl):
prop1, prop2 = rep(prop1), rep(prop2)
for i in r_TT(len(var_list),"",len(var_list)):
p1, p2 = prop1 , prop2
for j in range(len(vl)):
p1,p2 = p1.replace(vl[j],i[j]), p2.replace(vl[j],i[j])
if eval(p1.replace("T","True").replace("F","False")) != eval(p2.replace("T","True").replace("F","False")):
return False
return True