逻辑否定在Prolog中
我已经阅读了很多关于Prolog的失败否定的文章，其中Prolog为了证明“ +Goal持有”试图证明Goal失败。
这与CWA （密切的世界假设）高度相关，例如，如果我们查询+P(a) （其中P是秩序1的谓词）并且我们没有导致证明P(a)线索，到CWA） not P(a)持有，所以+P(a)成功。
从我搜索的这个方法来解决古典逻辑弱点，如果我们不知道P(a)那么我们就无法回答+P(a)是否成立。
以上描述的是在Prolog中引入非单调推理的方式。 此外，有趣的部分是克拉克证明，失败否定与古典否定仅仅适用于相似条款。 我明白，例如：
X=1, +X==1. ：应该在Prolog（和古典逻辑）中返回false。
+X==1, X=1. ：在经典逻辑中应该返回false，但在检查NF之后，它在Prolog中成功X不受限制，这与Classic-Pure Logic不同。
+X==1. ：直到X被绑定之前，不应该在经典逻辑中给出任何答案，但是在Prolog中，它返回假（可能打破经典逻辑的弱点），并且这与纯逻辑不相同/兼容。
我的目的是模拟经典否定，感谢@ false在评论中的建议，目前的实现是：
+(Goal) :- when(ground(Goal), +Goal).
一些测试：
?- +(X==1).
when(ground(X), +X==1).
?- X=1, +(X==1).
false.
?- +(X==1), X=1.
false.
我的问题：
上述是对经典否定的正确解释吗？ （是否有任何明显的角落案例，它错过了??我也关心逻辑纯度何时使用/ 2，是否安全地认为上述是纯粹??）。
Prolog不能做古典否定。 因为它不使用经典推理。 即使克拉克完成，它也无法检测到以下两个经典法则：
不矛盾的法则：〜（p / 〜p）
排除中间法：p /〜p
这里是一个例子，拿这个逻辑程序和这些查询：
p :- p
?- +(p, +p)
?- p; +p
逻辑程序的Clark完成如下，作为失败查询执行的否定产生以下结果：
p <-> p
loops
loops
克拉克完成了基于谓词定义和负面信息的问题。 另见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，...取代。
但对CLP（FD）的否定通常在适用于约束（in）/ 2时不起作用。 如果CLP（X）系统提供物化，情况可以稍微缓和。 在这种情况下，分离可以比使用Prolog回溯析取更加智能。
链接地址: http://www.djcxy.com/p/66947.html