用python解决归结反演的问题

一、实验目的

二、实验思路

第一步：先将子句集转换为数字表示，这样利于判断归并，相加为0即可
第二步：从子句集中取出2个进行归并判断
第三步：完成判断后进行移除数据和查重处理，然后将新子句集加入总子句集中
第四步：判断总子句集中的最后一个元素是否为空，为空的话证明归结成功

三、代码及注解

# 非用字符~表示，析取用大写v表示 a=in put("请输入子句集：")X=[ ]
X=[]
a = input("请输入子句集：")
while a != "0":x = a.split("V")for i in range(len(x)):if x[i] == "P(A)":x[i]=1elif x[i] =="P(B)":x[i]=2elif x[i] == "P(C)":x[i]=3elif x[i] == "~P(B)":x[i]=-2elif x[i] == "~P(A)":x[i]=-1elif x[i] == "~P(C)":x[i]= -3X.append(x)a = input("请输入子句集：")
print(X)# 对加入的归并后产生的子句集列表进行去重
def doubleRemove (o=[]):length1 = 0while length1 != len(o):length1 = len(o)for i in range(len(o)):if i< len(o):for j in range(i+ 1 ,len(o)):if j < len(o):if o[i]==o [j]:o.remove(o[i])return o# 从中总的子句集列表中取出2个子句集，判断是否能够去重
def guiJie (s=[], q=[]):length3 = len(s + q)for i in s:for j in q:if i + j == 0:s.remove(i)q.remove(j)if length3 != len(s + q):return doubleRemove(s + q)else:return 0# length为X的长度
length = 0
while length != len(X):length = len(X)for i in range(len(X)):for j in range(i + 1, len(X)):return_value = guiJie(X[i], X[j])if return_value != 0:X.append(return_value)doubleRemove(X)if not X[-1]:print("推理成功")
else:print("推理失败")