Prolog中的逻辑否定

Question

我已经阅读了很多关于Prolog的失败否定的内容,其中Prolog是为了证明\+Goal持有试图证明Goal失败.

这与CWA(近距离世界假设)高度相关,例如,如果我们查询\+P(a)(在哪里P是arity 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,但是在检查NF的时候它在Prolog中成功,X不受约束,这与classic-Pure Logic不同.

\+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. 

我的问题:

以上是对经典否定的正确解释吗？(是否有任何明显的极端情况,它错过了？当使用/ 2时我也关注逻辑纯度,可以安全地假设上面是纯粹的吗??).

Answer 1

Prolog 无法进行经典否定。因为它不使用经典推理。即使存在克拉克完成，它也无法检测到以下两个经典定律：

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

排中律：p \/ ~p

这是一个例子，采用这个逻辑程序和这些查询：

   p :- p

   ?- \+(p, \+p)

   ?- p; \+p

逻辑程序的 Clark 补全如下，作为失败查询执行的否定结果如下：

   p <-> p

   loops

   loops

克拉克完成解决了谓词定义和负面信息的问题。另请参阅第5.2 节“规则及其完成”。另一方面，当周围没有谓词定义时，当否定运算符被定义为 deMorgan 风格时，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, ... 替换。

但当应用于约束 (in)/2 时，CLP(FD) 的否定通常不起作用。如果 CLP(X) 系统提供具体化，这种情况可以稍微缓解。在这种情况下，析取可以比仅使用 Prolog 回溯析取更加智能。