序言否定和逻辑否定

Question

假设我们有以下程序:

a(tom). 
v(pat).

和查询(返回 false):

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

跟踪时，我可以看到 X实例化为 tom , 谓词 a(tom)成功，因此 \+ a(tom)失败。
我在一些教程中读到 Prolog 中的 not ( \+ ) 只是一个测试，不会导致实例化。

有人可以为我澄清上述观点吗？正如我所看到的实例化。

我知道不(否定为失败)和逻辑否定之间存在差异。您能否引用一篇解释它们在哪些情况下表现相同以及何时表现不同的好文章？

Answer 1

很好的问题。

简短的回答:你偶然发现了“挣扎”。

The problem is that the implementation of the operator \+ only works when applied to a literal containing no variables, i.e., a ground literal. It is not able to generate bindings for variables, but only test whether subgoals succeed or fail. So to guarantee reasonable answers to queries to programs containing negation, the negation operator must be allowed to apply only to ground literals. If it is applied to a nonground literal, the program is said to flounder. link

如果您反转查询
v(X), \+ a(X).
你会得到正确的答案。一些实现或元解释器检测到陷入困境的目标并延迟它们，直到所有变量都被确定。

关于您的观点 1)，您会看到 NAF 树内的实例化。在那里发生的事情不应该影响外部变量(在这种情况下是 v(X))。 Prolog 经常以天真的方式来避免低效率。理论上它应该只返回一个错误而不是实例化变量。

2) 这是我最喜欢的关于该主题的文章: Nonmonotonic Logic Programming .