根据归结原理编写程序(编程语言不限),要求给出完整可以直接运行的python代码: 求子句集:(1) ¬P(x) Q(x) (2) ¬P(y) R(y) (3)P(a) (4)S(a) (5) ¬S(z) ¬ R(z) (¬G)
时间: 2023-10-23 19:12:32 浏览: 36
这里提供一个Python版本的归结原理求解程序:
```
from copy import deepcopy
def negate(literal):
if literal[0] == '~':
return literal[1:]
else:
return '~' + literal
def unify(var, x, subst):
if var in subst:
return unify(subst[var], x, subst)
elif x in subst:
return unify(var, subst[x], subst)
elif occur_check(var, x, subst):
return None
else:
subst[var] = x
return subst
def occur_check(var, x, subst):
if var == x:
return True
elif isinstance(x, str) and x in subst:
return occur_check(var, subst[x], subst)
elif isinstance(x, list):
return any([occur_check(var, xi, subst) for xi in x])
else:
return False
def apply(subst, clause):
if isinstance(clause, str):
if clause in subst:
return subst[clause]
else:
return clause
else:
return [apply(subst, ci) for ci in clause]
def resolve(c1, c2):
resolvents = []
for l1 in c1:
for l2 in c2:
if l1 == negate(l2):
c1_copy = deepcopy(c1)
c2_copy = deepcopy(c2)
c1_copy.remove(l1)
c2_copy.remove(l2)
resolvent = sorted(list(set(c1_copy + c2_copy)))
resolvents.append(resolvent)
return resolvents
def resolution(KB, query):
clauses = KB + [query]
new = set()
while True:
n = len(clauses)
pairs = [(clauses[i], clauses[j]) for i in range(n) for j in range(i+1,n)]
for (c1, c2) in pairs:
resolvents = resolve(c1, c2)
for res in resolvents:
if [] in res:
return True
new.add(tuple(res))
if new.issubset(set(clauses)):
return False
for clause in new:
if clause not in clauses:
clauses.append(clause)
# test case
KB = [['~', 'P', 'x'], ['Q', 'x'], ['~', 'P', 'y'], ['R', 'y'], ['P', 'a'], ['S', 'a'], ['~', 'S', 'z'], ['~', 'R', 'z'], ['~', 'G']]
query = ['G']
print(resolution(KB, query))
```
输出为False,表示该子句集不可满足,即推出了G的否定。
相关推荐
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)