一阶逻辑统一

Posted 2023-05-08

【中文标题】一阶逻辑统一

【英文标题】：First Order Logic Unification

【发布时间】：2019-07-04 01:32:43

【问题描述】：

我有一个关于 FOL 练习的问题，我必须证明是否可以统一两个句子，并在肯定的情况下展示如何统一它们。

1) f(g(a,X),g(Y,Y))=f(g(a,b),g(f(a),f(Z)))

2) f(cons(cons(a,b)))=f(cons(cons(a,nil))

对于第一个，我理解了过程，所以我将值 f(a) 赋予了 Z，然后我使用了 substitution o = Y/f(a) 得到两个相同的句子。

对于第二个，我真的不明白句子的语义是什么，如何统一它。

【参考方案1】：

统一算法很简单

如果两边都是常数（数字、字符串、原子等），则结果统一起来就是同一个 如果一侧是变量，我们添加另一侧对这个变量的代入 如果双方都是函数，则统一这是否是相同的函数（相同的名称）和相同的奇偶校验（参数个数），然后递归地统一参数。

用你的例子：

f(g(a,X),g(Y,Y)) = f(g(a,b),g(f(a),f(Z))) 第三种情况，相同的功能（f）和相同的数量（2）。所以要统一参数：

g(a,X) = g(a,b) g(Y,Y) = G(f(a), f(Z))

g(a,X) 与 g(a,b) 统一，因为这是相同的函数 (g) 相同的数量 (2)。 a = a 统一（案例 1），X = b 统一（案例 2）与替换 X/b

G(Y,Y) 与 G(f(a), f(Z)) 统一，因为这是相同的函数 (g) 相同的数量 (2)。然后 Y=f(a) => 替换 Y/f(a) 和 Y=f(Z) => f(a) 与 F(Z) Z/a

最后你得到 o = X/b, Y/f(a), Z/a

f(cons(cons(a,b))) = f(cons(cons(a,nil)))

这里也一样。相同的功能（f）相同的数量（1）。统一 cons(cons(a,b)) = cons(cons(a,nil)) 相同的功能（缺点）相同的数量（1）。统一 cons(a,b) = cons(a,nil) 相同的功能（缺点），相同的数量（2）。统一 a=a (OK), b=nil => NO

这不统一。