prolog - 为什么双重否定在 Prolog 中不绑定(bind)

Question

假设我有以下理论:

a(X) :- \+ b(X).

b(X) :- \+ c(X).

c(a).

它只是说真的，这当然是正确的，a(X)是真的，因为没有 b(X) (以否定作为有限失败)。由于只有 b(X)如果没有c(X)我们有 c(a) ，可以说这是真的。但是我想知道为什么 Prolog 不提供答案 X = a ?比如说我介绍了一些语义:

noOrphan(X) :- \+ orphan(X).

orphan(X) :- \+ parent(_,X).

parent(david,michael).

当然，如果我查询 noOrphan(michael) ，这将导致 true和 noOrphan(david)在 false (因为我没有为 david 定义父级)。但我想知道为什么没有主动方法来检测哪些人( michael ，david ，...)属于 noOrphan/1关系？

这可能是 Prolog 的回溯机制的结果，但是 Prolog 可以保持一种状态，该状态可以验证一个人是在以积极的方式(0,2,4,...)深度否定，还是以消极的方式(1,3 ,5,...) 深度否定。

Answer 1

让我们从更简单的事情开始。说\+ X = Y .在这里，否定的目标是一个预定义的内置谓词。所以事情就更清楚了:X和 Y应该不同。但是，\+ X = Y失败，因为 X = Y成功。因此，没有留下任何痕迹，目标是在哪个精确条件下失败。

因此，\+ \+ X = Y确实会产生一个空答案，而不是预期的 X = Y . See this answer for more .

鉴于这种简单的查询已经显示出问题，您不能对像您这样的用户定义目标抱有太多期望。

在一般情况下，您必须首先重新考虑否定的实际含义。答案比乍看起来要复杂得多。想想程序p :- \+ p.应该 p成功还是失败？应该 p是真的还是假的？这里实际上有两个模型不再适合 Prolog 使用最小模型的观点。这些考虑为逻辑编程开辟了新的分支，如答案集编程 (ASP)。

但让我们坚持使用 Prolog。否定只能在非常有限的上下文中使用，例如当目标被充分实例化并且定义被分层时。不幸的是，没有普遍接受的标准来安全执行被否定的目标。我们可以等到目标是可变的(地面)，但这通常意味着我们必须等待太久——用行话来说:被否定的目标陷入困境。

如此有效，一般否定与纯 Prolog 程序配合得不是很好。 Prolog 的核心确实是该语言的纯粹、单调的子集。不过，在 Prolog(或其各自的扩展)的约束部分内，否定可能会很好地工作。