问题描述
标签 logical purity 提到 (=)/2 是纯的。是吗 “本质上”纯还是“操作”纯？到 据我所知，它可以由这个 Horn 子句定义：
∀x(=(x,x))
这是 Prolog 的事实，如果还不是内置的：
X = X.
这意味着 (=)/2 将是“本质上”纯的，因为 SWI-Prolog 已经 remarks。那么什么是 那么一阶等式的差 (FOL=)，如果有 有什么不同吗？
解决方法
我猜 (=)/2 的“intrinsinc”定义确实确保了统一谓词是自反的、对称的和可传递的。 FOL= 也满足的要求。但是 FOL= 也需要一致，就是这个 axiom schema:
/* 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
在所谓的 unification modulo theories 中情况有所不同，unification 和 unify 谓词可能会改变它们的含义。