Prolog中的逻辑否定

Question

我已经阅读了很多关于 Prolog 的 Negation by Failure 的内容，其中 Prolog 为了证明 \+Goal 成立试图证明 Goal 失败。

这与 CWA（近距离假设）高度相关，例如，如果我们查询 \+P(a)（其中 P 是元数 1 的谓词），我们没有任何线索可以导致证明P(a) Prolog 假设（由于 CWA）not P(a) 成立，所以\+P(a) 成功。

根据我的搜索，这是一种解决经典逻辑弱点的方法，如果我们不知道P(a)，那么我们就无法回答\+P(a) 是否成立。

上面描述的是在 Prolog 中引入非单调推理的方式。此外，有趣的部分是 Clark 证明了 Negation by Failure 与经典否定仅适用于基础条款兼容/相似。我理解例如：

X=1, \+X==1.: 在 Prolog（和经典逻辑）中应该返回 false。

\+X==1, X=1.: 在经典逻辑中应该返回 false，但它在 Prolog 中成功，因为检查 NF 的时间X 未绑定，这与经典纯逻辑不同。

\+X==1.：在绑定X 之前，不应在经典逻辑中给出任何答案，但在 Prolog 中它返回 false（可能是为了打破经典逻辑的弱点），这与纯逻辑不同/不兼容。

我的尝试是模拟经典的否定，感谢@false 在 cmets 中的建议，目前的实现是：

\\+(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 不能进行经典否定。由于它不 使用经典推理。即使在克拉克面前 完成后，它无法检测到以下内容 两条经典定律：

不矛盾定律：~(p /\ ~p)

排中律：p \/ ~p

这里是一个例子，取这个逻辑程序 以及这些查询：

   p :- p

   ?- \+(p, \+p)

   ?- p; \+p

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

   p <-> p

   loops

   loops

Clark 补全解决了谓词定义的问题 和负面信息。另见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 回溯析取更智能一点。

Answer 2

在SWI-Prolog中，可以实现Constraint Handling Rules中的经典逻辑推理规则，包括德摩根定律和不矛盾定律：

:- 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。