使用否定时，子句主体的 Prolog 顺序会给出不同的结果

Question

我很难理解为什么当其中一个子句是否定时交换两个主体子句会给出不同的结果。

married(john).
male(john).
male(kev).

bachelor1(X) :- \+ married(X), male(X).
bachelor2(X) :- male(X), \+ married(X).

bachelor1(X).

没有找到任何原子。

bachelor2(X).

找到 kev。

Answer 1

运算符

\+

（助记符：⊬）实现非单调推理规则（称为“否定即失败”），仅针对“ground”目标表达逻辑否定。根据这条规则，只有当目标 \+(G) 无法被证明时，G 才为真。换句话说，为了证明

\+(G)

，Prolog 首先尝试证明

G

，然后：

如果

G

成功
• ，则

  \+(G)

  失败；如果G
失败
• ，则

  \+(G)

  成功。 正如我们所见，对于没有变量的查询，谓词 bachelor1/1
和

bachelor2/1

都能按预期工作：

?- bachelor1(john).
false.

?- bachelor1(kev).
true.

?- bachelor2(john).
false.

?- bachelor2(kev).
true.

事实上，这个问题只发生在包含变量的查询中。要了解

bachelor1/1

 和 

bachelor2/1

之间的区别，请分析以下 Prolog 搜索树：

在第一个版本中，要证明的否定目标

不是

地面（因此，谓词无法按预期工作）。

在第二个版本中，要证明的否定目标是

地面（因此，谓词确实按预期工作）。