prolog - 寻求 (\=)/2 的纯 Prolog 实现

Question

作为失败的否定通常被认为是不纯的。否定失败所需的 Prolog 解释器必须实现 SLDNF，它是 SLD 的扩展。

谓词(\=)/2例如在 library(reif) 中使用。它可以通过否定作为失败引导，如下所示，但通常是内置的：

X \= Y :- \+ X = Y.

是否可以(\=)/2作为纯谓词来实现？仅使用纯 Prolog，即仅使用一阶喇叭子句？

Answer 1

是否可以将 (=)/2 实现为纯谓词？仅使用纯 Prolog，即仅使用一阶喇叭子句？

你不能(\=)/2在纯 Prolog 中实现。

证明：

在逻辑上，合取是可交换的，纯 Prolog 查询，如果它们终止，则必须是合乎逻辑的。

但是，对于(\=)/2，术语的顺序很重要，因此不合逻辑：

?- X \= Y, X=0, Y=1.
false.

?- X=0, Y=1, X \= Y.
X = 0,
Y = 1.