编写函数 MGU实现最一般合一算法. 该函数要点如下: 输入为两个原子公式, 它们的谓词相同. 其数据类型为 str,输出最一般合一的结果, 数据类型为 dict, 格式形如{变量: 项, 变量: 项}, 其中的变 量和项均为字符串. 若不存在合一, 则返回空字典

def MGU(s1, s2):
# 若两个原子公式相同, 则返回空字典
if s1 == s2:
return {}
# 将两个原子公式分割成谓词和参数
p1, args1 = s1.split('(')
args1 = args1.rstrip(')').split(',')
p2, args2 = s2.split('(')
args2 = args2.rstrip(')').split(',')
# 若两个原子公式的谓词不同, 则返回空字典
if p1 != p2:
return {}
# 初始化替换字典
subs = {}
# 遍历参数列表, 对相同位置的参数进行统一替换
for i in range(len(args1)):
# 若参数相同, 则不用替换
if args1[i] == args2[i]:
continue
# 若参数是变量, 则将其加入替换字典中
if args1[i].islower():
subs[args1[i]] = args2[i]
elif args2[i].islower():
subs[args2[i]] = args1[i]
# 若参数既不相同也不是变量, 则无法合一, 返回空字典
else:
return {}
# 返回替换字典
return subs