5

假设我们有以下程序：

a(tom). 
v(pat).

和查询（返回false）：

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

跟踪时，我可以看到X实例化为tom，谓词a(tom)成功，因此\+ a(tom)失败。

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

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

  2. 我知道非（否定为失败）和逻辑否定之间存在差异。您能否参考一篇好文章来解释它们在哪些情况下表现相同以及何时表现不同？

4

2 回答 2

3

好问题。

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

问题是运算符 \+ 的实现仅在应用于不包含变量的文字（即基本文字）时才有效。它不能为变量生成绑定，只能测试子目标是成功还是失败。因此，为了保证对包含否定的程序的查询做出合理的回答，必须允许否定运算符仅适用于基本文字。如果将其应用于非地面文字，则该程序被称为挣扎。 关联

如果您反转查询

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

你会得到正确的答案。一些实现或元解释器检测到挣扎的目标并延迟它们，直到所有变量都被接地。

关于您的第 1 点），您会看到 NAF 树内的实例化。那里发生的事情不应该影响外部变量（在本例中为 v(X)）。Prolog 经常以幼稚的方式行事，以避免效率低下。理论上它应该只返回一个错误而不是实例化变量。

2) 这是我最喜欢的关于该主题的文章：非单调逻辑编程。

于 2013-02-06T11:28:06.450 回答
1

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

您已经体验到理解 NAF 可能很困难。部分原因可能是（逻辑）否定，即使在谓词演算的简单竞赛中也很难定义（例如参见Russel 悖论），部分原因是 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 的工作原理

于 2013-02-05T20:22:51.660 回答