Prolog中的逻辑否定

Question

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

这与CWA（close world assumption）密切相关，例如，如果我们查询\+P（a）（其中P是一元谓词），并且没有线索表明P（a）成立，则Prolog假设（由于CWA）not P（a）成立，因此\+P（a）成功。

从我所搜索的内容来看，这是解决古典逻辑弱点的一种方法，因为如果我们对P（a）一无所知，那么我们就无法回答\+P（a）是否成立。

上述内容是引入Prolog非单调推理的方式。此外，有趣的是Clark证明了Negation by Failure与经典否定只在ground clauses中兼容/相似。我理解，例如：

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时，我关心逻辑纯度，可以安全地假设上述内容是纯的吗？）。

- coder

---

ground/2 没有任何意义。 - false

一个关系的含义由其基础解释所定义。即对于该关系成立的基础术语的集合。因此，ground/2 必须恒为真。没有任何情况下它会是假的。 - false

没问题，我会尽力让翻译更加通俗易懂但不改变原意：那很有道理。 - false

这是一种非单调扩展形式。不管它的优点如何，坚持地要求groundness（全局变量）限制了它的使用范围。大多数情况下，答案会是一个floundering（不稳定）的目标，这并没有告诉你任何有用信息。想想目标\\+([]=[X|Xs])，因为它不是全局变量，所以你将永远得不到响应，而dif([], [X|Xs])则可以顺利成功。 - false

顺便说一句，你的问题值得更详细的回答，这个回答将从1972年和Prolog 0开始，涵盖到现在发生的所有事情，包括ASP，但也包括Prolog本身的纯编程。 - false

Answer 1

Prolog无法进行经典否定，因为它不使用经典推理。即使在Clark补全的存在下，它也不能检测到以下两个经典规律：

非矛盾律：~（p /\ ~p）

排中律：p \/ ~p

这里有一个例子，看看这个逻辑程序和这些查询：

   p :- p

   ?- \+(p, \+p)

   ?- p; \+p

逻辑程序的Clark完成如下，否定查询执行结果如下：

   p <-> p

   loops

   loops

Clark补全解决了谓词定义和否定信息的问题。请参阅第5.2节规则及其补全。另一方面，当没有谓词定义时，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约束替换。

但是，当应用于(in)/2约束时，对于CLP(FD)来说否定通常不起作用。如果CLP(X)系统提供具备实现能力，情况可以稍微缓解。在这种情况下，可以使析取比使用Prolog回溯析取更智能一些。

- user502187

---

Prolog并不是传统的，而更像是直觉主义逻辑，其中标签“true”表示“可证明/有证据支持”（与经典逻辑中由上帝发出的语句“true”相对），这种情况被Lambda Prolog所接受。我不明白为什么每本关于Prolog的书都不把这个放在第一位。 - David Tonhofer

直觉主义逻辑要求“非矛盾律：~（p /\ ~p）”，这在直觉主义逻辑中是可证明的。因此，Prolog低于直觉主义逻辑，可以证明它是所谓的最小逻辑的一个片段。 - user502187

Answer 2

在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）可以更高效地解决这个公式。

- Anderson Green

---

我只是想问一下，“使Prolog经典化”的整个项目如何与一阶逻辑不可判定的事实相吻合。 - tiffi