Prolog否定和逻辑否定

Question

假设我们有以下程序:

a(tom). 
v(pat).

和查询(返回false):

\+ a(X), v(X).

在跟踪时,我可以看到X被实例化为tom,谓词a(tom)成功,因此+ a(tom)失败.

我在一些教程中读到,Prolog中的not(+)只是一个测试而不会导致实例化.

1. 有人可以请我澄清以上几点吗？我可以看到实例化.

2. 我知道not(否定为失败)和逻辑否定之间存在差异.您能否参考一篇好文章来解释他们在哪些情况下表现相同以及他们什么时候表现不同？

Answer 1

WRT 点 2，维基百科文章似乎是一个很好的起点。

您已经体验到理解 NAF 可能很困难。部分原因可能是因为（逻辑）否定本质上很难定义，即使在谓词微积分的更简单的竞赛中（例如参见罗素悖论），部分原因是 Prolog 的强大变量被限制为保留失败证明的实际反例。看看您是否可以理解forall /2的实际库定义（请阅读文档，它是合成的且有趣的），这是运行故障驱动循环的首选方法：

%%  forall(+Condition, +Action)
%
%   True if Action if true for all variable bindings for which Condition
%   if true.

forall(Cond, Action) :-
    \+ (Cond, \+ Action).

我记得第一次看到它的时候，它看起来就像魔法一样......

编辑一个教程时，我在“探索”我的链接集合时发现，JRFisher 是一个很好的网站。它充满了有趣的东西，可惜解释有点简洁，需要学生通过频繁的练习来回答自己。请参阅第2.5 段，专门讨论失败否定。我想你也可以喜欢第 3 节：Prolog 是如何工作的