prolog - Prolog中的逻辑否定

Question

我已经阅读了很多关于 Prolog 的 失败否定其中Prolog为了证明\+Goal持有试图证明 Goal失败。
这与 高度相关CWA (近距离假设)例如，如果我们查询 \+P(a) (其中 P 是元数 1 的谓词)并且我们没有线索可以证明 P(a) Prolog 假设(由于 CWA)not P(a)如此\+P(a)成功。
根据我的搜索，这是一种解决经典逻辑弱点的方法，如果我们不知道 P(a)那么我们无法回答是否 \+P(a)持有。
上面描述的是在 Prolog 中引入非单调推理的方式。此外，有趣的部分是 克拉克 证明了 Negation by Failure 与经典否定仅适用于基础条款兼容/相似。我理解，例如:X=1, \+X==1. : 应该在 Prolog(和经典逻辑)中返回 false。\+X==1, X=1. : 在经典逻辑中应该返回 false，但它在 Prolog 中成功，因为检查 NF X不受约束，这与经典的纯逻辑不同。\+X==1. : 在 X 之前不应该在经典逻辑中给出任何答案是绑定(bind)的，但在 Prolog 中它返回 false(可能是为了打破经典逻辑的弱点)，这与纯逻辑不同/不兼容。
我的尝试是模拟经典否定，感谢@false 在评论中的建议，目前的实现是:

\\+(Goal) :- when(ground(Goal), \+Goal). 

一些测试:

?- \\+(X==1).
when(ground(X), \+X==1).

?- X=1, \\+(X==1).
false.

?- \\+(X==1), X=1.
false. 

我的问题:
以上是对经典否定的正确解释吗？
(它是否遗漏了任何明显的极端情况？？我也担心使用 when/2 时的逻辑纯度，可以安全地假设以上内容是纯的吗？？)。

Answer 1

Prolog 不能做经典的否定。由于它不
使用经典推理。即使在克拉克面前
完成后，它无法检测到以下内容
两条经典定律:

Law of noncontradiction: ~(p /\ ~p)

Law of excluded middle: p \/ ~p

这是一个例子，拿这个逻辑程序
和这些查询:

   p :- p

   ?- \+(p, \+p)

   ?- p; \+p

逻辑程序的克拉克完成是
如下，否定为失败查询
执行产生以下结果:

   p <-> p

   loops

   loops

克拉克完成解决了谓词定义的问题
和负面信息。另见部分 5.2 Rules and their Completion .另一方面，当没有谓词时
有定义，CLP(X) 有时可以同时执行这两个定律，
当一个否定运算符被定义为 deMorgan 风格时。这是
CLP(B) 的否定运算符:

?- listing(neg/1).
neg((A;B)) :-
    neg(A),
    neg(B).
neg((A, _)) :-
    neg(A).
neg((_, A)) :-
    neg(A).
neg(neg(A)) :-
    call(A).
neg(sat(A)) :-
    sat(~A).

这是一些执行:

?- sat(P); neg(sat(P)).
P = 0 
P = 1.
?- neg((sat(P), neg(sat(P)))).
P = 0 
P = 1.

当否定影响域时，CLP(X) 也会出现问题，
通常是有限的，然后会变得无限。因此对于
例如一个约束，如 (#=)/2, ... 不应该是一个问题，
因为它可以被一个约束 (#\=)/2, ... 替换。

但是当应用于约束时，对 CLP(FD) 的否定通常不起作用
(中)/2。如果 CLP(X) 系统提供
物化。在这种情况下，析取可以比仅使用 Prolog 回溯析取更智能一点。