prolog - 统一谓词 (=)/2 与一阶相等有何不同？

Question

标签逻辑纯度提到 (=)/2 是纯的。它是“内在”纯粹还是“操作”纯粹？据我所知，它可以由这个 Horn 子句定义：

∀x(=(x, x))

如果还不是内置的，这是 Prolog 的事实：

X = X.

这意味着 (=)/2 将是“本质上”纯粹的，正如 SWI-Prolog 已经指出的那样。那么，如果有任何差异，那么与一阶相等（FOL=）有什么区别？

Answer 1

我猜 (=)/2 的“内在”定义确实确保了统一谓词是自反的、对称的和传递的。FOL= 也满足的要求。但是 FOL= 也需要一致性，这就是这个公理模式：

/* Predicate Congruence in FOL= */

∀x1..∀xn∀yj(=(xj, yj) & p(x1, .., xn) -> p(x1, .., xj-1, yj, xj+1, .., xn))

统一谓词的唯一 Horn 子句不代表这点。并且由于 unify 谓词是内置的，因此也不能添加缺少的 Horn 子句。那么会出什么问题呢？我们可以举一个会出错的例子吗？

经典的例子是这个事实：

p(morning_star).

显然，此查询在 Prolog 中成功：

?- p(morning_star).
true

但是这个查询在 Prolog 中失败了，而在 FOL= 中它会成功：

?- morning_star = evening_star, p(evening_star).
false

在所谓的统一模理论中情况有所不同，其中统一和统一谓词可能会改变它们的含义。