一阶谓词逻辑解析度 – 我的研究心得

实际上，正确和完整的分辨率微积分在20世纪70年代引发了逻辑上的兴奋。许多科学家认为，人们可以在PL1中制定知识表示和推理的几乎所有任务，然后用自动化的证明者来解决它。谓词逻辑，一种强大的表达语言，以及完整的证据演算似乎是用于表示知识和解决许多难题的通用智能机器（图 3.3 ）。

如果将一组公理（即知识库）和查询输入到这样的逻辑机器中作为输入，则机器搜索证明并返回它 – 对于一个存在并且将被找到 – 作为输出。以哥德尔的完备性定理和赫布兰德作为基础的工作为逻辑的机械化投入了很多。机器的愿景，可以与任意非矛盾的PL1知识库，证明任何真正的查询是非常诱人的。因此，到目前为止，PL1的许多证明结石正在开发并以其后的形式实现。作为一个例子，我们在这里描述历史上重要且广泛使用的分辨率演算并展示其功能。如上所述，选择分辨率作为证明微积分的一个例子的原因是其历史和教学重要性。今天，

首先，我们试图编译证明表 3.2 页 41 与实例的的知识库
3.2 成分辨率证明。首先将公式转换为合取范式和否定查询

¬ Q ≡¬ 孩子（前夕，奥斯卡，安妮）

被添加到知识库中，它给出了

KB ∧¬ Q ≡（子（前夕，安妮，奥斯卡））1 ∧

（¬子（X，Y，Z）∨子（X，Z，Y））2 ∧

（¬孩子（夏娃，奥斯卡，安妮））3。

然后证据可能看起来像

：¬∨

（2）x / eve，y / anne，z / oscar（儿童（夏娃，安妮，奥斯卡）

子（前夕，奥斯卡，安））4个RE（3，4）：（¬子（前夕，安，奥斯卡））5个 RES（1，5）：（）6，

其中，在第一步中，变量x，y，z被常量替换。然后在（2.2）的一般解决规则的应用下遵循两个解决步骤，其从命题逻辑中保持不变。

以下示例中的情况稍微复杂一些。我们假设每个人都认识自己的母亲并询问亨利是否认识任何人。用函数符号“ 母亲 ”和谓词“ 知道 ”，我们必须从中得出一个矛盾

（知道（X，母（X）））1 ∧（¬知道（亨利，Y））2。

通过替换x / henry，y / mother（henry），我们得到了矛盾的子句对

（知道（亨利，母亲（亨利）））1 ∧（¬知道（亨利，母亲（亨利）））2。

这个替换步骤称为统一。这两个文字是互补的，这意味着它们与标志不同。现在可以通过解决步骤推导出空子句，通过该步骤可以看出亨利确实认识某人（他的母亲）。我们定义

定义3.7如果所有变量都有替换σ ，那么两个文字就被称为可统一的，这使得文字相等。这种σ称为统一者。如果可以通过替换变量从其获得所有其他联合符，则将统一者称为最通用的统一者（MGU）。

例3.6 我们想统一文字 p（f（g（x）），y，z）和 p（u，u，f（u））。几个统一体是

σ 1 ： Y / F（G（X））中，z / F（F（G（X））），U / F（G（X）），σ 2 ： X / H（v）中，Y / F（ g（h（v））），z / f（f（g（h（v）））），u / f（g（h（v）））

σ 3 ： X / H（H（v））中，Y / F（G（H（H（v））中））中，z / F（F（克（H（H（V））））），U / f（g（h（h（v））））

σ 4 ： X / H（a）中，Y / F（G（H（A）））中，z / F（F（克（H（A）））），U / F（G（H（a））的）σ 5 ： X / A，Y / F（G（A））中，z / F（F（G（A））），U / F（G（A））

其中σ1是最通用的统一者。其他unifiers从导致σ通过置换1 X /小时（V）中，x / H（H（v））中，X /小时（一）中，x / A。

我们可以在这个例子中看到，在文字统一期间，谓词符号可以像函数符号一样对待。也就是说，文字被视为一个术语。统一算法的实现按顺序处理函数的参数。术语在术语结构上递归统一。在大多数情况下，最简单的统一算法非常快。然而，在最坏的情况下，计算时间会随着术语的大小呈指数级增长。因为对于自动化的证明，绝大多数的统一尝试失败或非常简单，在大多数情况下，最坏的情况复杂性没有显着的影响。即使在最坏的情况下，最快的统一算法也具有接近线性的复杂度[Bib82]。

我们现在可以给出谓词逻辑的一般解析规则：

定义3.8 联合正常形式的两个条款的解决规则

（A 1 ∨…∨上午∨ B），（¬乙∨ Ç 1 ∨…∨ Cn）的σ（B）= σ（B），（3.6）

（σ（A 1）∨・・・∨σ（Am）∨σ（C 1）∨・・・∨σ（Cn））

其中σ是B和B的MGU 。

定理3.5分辨率规则是正确的。也就是说，解决方案是两个父条款的语义后果。

但是，对于完整性，我们仍然需要一个小的添加，如以下示例所示。

例3.7 着名的拉塞尔悖论写道：“有一个理发师会刮掉每个不刮胡子的人。”这种说法是矛盾的，这意味着它是不可满足的。我们希望通过决议来表明这一点。悖论在PL1中形式化

∀ X剃须（理发，X）
⇔¬ 剃须（X，X）

并转换为子句形式的收益率（参见第 55 页的练习 3.6 ）

（¬剃须（BARBIER，X）∨¬剃须（X，X））1 ∧（剃须（BARBIER，X）∨剃须（X，X））2。

（3.7）

从这两个条款中我们可以得出几个重言式，但没有矛盾。因此，解决方案尚未完成。我们还需要一个进一步的推理规则。

定义3.9 条款的分解是通过以下方式完成的

（A 1 ∨阿2 ∨…∨ An）的σ（A 1）= σ（A 2），（σ（A 2 ）∨…∨ σ（安））

其中σ是A 1和A 2 的MGU 。

现在矛盾可以从（ 3.7 ）得出

FAK（1，σ ： X /理发）：（¬剃须（理发，理发））3

Fak（2，σ ： x / barber）🙁刮胡子（理发师，理发师））4

RES（3，4）：（）5

我们声称：

定理3.6分解规则（3.6 ）与分解规则（3.9 ）一起反驳完成。也就是说，通过应用因子分解和分解步骤，空子句可以从任何不可满足的公式中得出。

1. 解决策略

∧¬

虽然分辨率的完整性对于用户来说很重要，但在实践中搜索证据可能非常令人沮丧。原因是巨大的组合搜索空间。即使在开始时KB Q中只有非常少的子句对，证明者也会在每个分辨率步骤中生成一个新子句，这会增加下一次迭代中可能的解决步骤的数量。因此，长期以来一直试图使用特殊策略来减少搜索空间，最好不会失去完整性。最重要的策略如下。

单位分辨率优先考虑解决步骤，其中两个条款中的一个只包含一个文字，称为单位条款。在许多情况下，这种策略保留了完整性并导致了搜索空间的减少，但并非总是如此。因此，它是一个启发式过程（见第6.3节）。

∧¬

通过应用一组支持策略，可以确保减少搜索空间。这里KB Q的子集被定义为支持集（SOS）。每个决议步骤都必须包含SOS中的条款，并将解决方案添加到SOS中。这个策略不完整。如果在没有SOS的情况下确保条款集合可以满足，则完成（参见第55 页的练习3.7）。否定查询Q通常用作初始SOS。

∧¬

在输入分辨率中，每个分辨率步骤都必须包含输入集KB Q中的子句。这种策略也减少了搜索空间，但代价是完整性。

使用纯文字规则可以删除包含其他子句中没有补充文字的文字的所有子句。此规则缩小了搜索空间并且完整，因此几乎所有分辨率证明器都使用它。如果条款K 1的文字表示条款K 2 的文字的子集，

然后可以删除K 2。例如，该条款

（下雨（今天）⇒街道_潮湿（今天））

如果street _ wet（今天）已经有效，则是多余的。这个重要的减少步骤称为包含。包容也是完整的。

2.
平等

¬=∨=

平等是搜索空间爆炸性增长的一个特别不方便的原因。如果我们增加（ 3.1 页） 36 和（制定了平等公理
3.2 页） 36 到知识库，则对称条款xyyx 可以与每一个正或否定式的统一，例如。这导致了新的子句和方程的推导，在这些子句和方程上可以再次应用相等公理，等等。传递性和替代公理具有类似的结果。正因为如此，已经开发出了相等的特殊推理规则，这些规则在没有明确的平等公理的情况下得以实现，特别是减少了搜索空间。解调，