我读过很多关于Prolog的失败否定的文章，Prolog为了证明+Goal成立，试图证明Goal失败了。
这与CWA(闭合世界假设)高度相关，例如，如果我们查询+P(a)(其中P是arity 1的谓词)，并且我们没有任何线索可以证明Prolog假设P(a)(由于CWA)not P(a)成立+P(a)成功。
从我所搜索的内容来看，这是一种解决经典逻辑弱点的方法，如果我们对P(a)一无所知，那么我们就无法回答+P(a)是否成立。
上面描述的是在Prolog中引入非单调推理的方式。此外，有趣的是，克拉克证明了失败否定与经典否定仅对基本从句兼容/相似。我理解例如：
X=1, +X==1.： 应该在 Prolog(和经典逻辑)中返回 false。
+X==1, X=1.： 应该在经典逻辑中返回 false，但它在 Prolog 中成功，因为检查 NF 的时间X不受约束，这与经典纯逻辑不同。
+X==1.：在X被绑定之前，不应该在经典逻辑中给出任何答案，但在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时，我也担心逻辑纯度，是否可以安全地假设上述内容是纯的？？
Prolog不能做经典的否定。因为它没有 使用经典推理。即使在克拉克面前 完成时，它无法检测到以下内容 两个经典定律：
不矛盾定律： ~(p/\ ~p)
排除中间定律：p \/~p
这里举个例子，拿这个逻辑程序来说 以及这些查询：
p :- p
?- +(p, +p)
?- p; +p
逻辑程序的克拉克完成是 如下和否定为失败查询 执行会产生以下结果：
p <-> p
loops
loops
克拉克补全解决了谓词定义的问题 和负面信息。另见第5.2节 规则和 他们的完成。另一方面，当没有谓词时 定义在周围，CLP(X)有时可以同时做这两个定律， 当否定运算符被定义为德摩根风格时。这是 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 回溯析取更智能一些。
在SWI-Prolog中，可以在约束处理规则中实现经典逻辑的推理规则，包括德摩根定律和不矛盾定律：
:- use_module(library(chr)).
:- chr_constraint is_true/1.
:- chr_constraint animal/2.
:- initialization(main).
:- set_prolog_flag('double_quotes','chars').
is_true(A),is_true(A) <=> is_true(A).
is_true(A=B) ==> A=B.
is_true(A=B) ==> not(A=B).
is_true(not(A)),is_true(A) ==> false.
is_true(not((A;B))) ==> is_true((not(A),not(B))).
is_true(not((A,B))) ==> is_true((not(A);not(B))).
is_true((A,B)) ==> is_true(A),is_true(B).
is_true((A;B)) ==> is_true(A),(is_true(B);is_true(not(B)));is_true(B),(is_true(A);is_true(not(A))).
is_true(not(not(A))) ==> is_true(A).
然后，您可以像这样使用求解器：
is_true(animal(X,A)),is_true(animal((Y,A))) ==> X = Y,false;X==Y.
is_true((A->B)) ==> is_true(((A;not(A)),B));is_true(((not(A);A),not(B))).
main :- is_true(((X=cat;X=dog;X=moose),(not((animal(dog,tom);animal(moose,tom))),animal(X,tom)))),writeln(animal(X,tom)).
该程序打印animal(cat,tom)。
但是这个公式可以使用不同的算法(如DPLL)更有效地求解。