分辨率定理证明

先决条件：

• 人工智能 |证明命题定理的证明和推论
• Wumpus 人工智能世界

在本文中，我们将讨论使用推理规则的推理算法。迭代深化搜索是一种完整的搜索算法，它可以定位任何可实现的目标。然而，如果可用的推理规则不充分，则无法达到目标——不存在仅使用这些推理规则的证据。例如，如果消除了双条件消除规则，则上一节中的证明将失败。本部分介绍分辨率，一个单一的推理规则，当与任何完全搜索算法结合时，它会给出一个完整的推理方法。

在 wumpus 宇宙中，我们从解析规则的简化版本开始。看一下导致上图的步骤——代理从 [2,1] 到 [1,1]，然后到 [1,2]，在那里它闻起来很臭，但没有注意到微风。以下信息已添加到知识库中：

$\begin{array}{ll} R_{11}: & \neg B_{1,2} . \\ R_{12}: & B_{1,2} \Leftrightarrow\left(P_{1,1} \vee P_{2,2} \vee P_{1,3}\right) \end{array}$

我们现在可以使用与之前导致 R10 相同的方法来推断 [2,2] 和 [1,3] 中缺少凹坑（请记住，[1,1] 已经知道是无凹坑的）：

$\begin{array}{ll} R_{13}: & \neg P_{2,2} \\ R_{14}: & \neg P_{1,3} \end{array}$

为了获得在[1,1]、[2,2]或[3,1]中存在坑的事实，我们可以对R3使用双条件消除，然后对R5使用Modus Ponens，如下：

$R_{15}: \quad P_{1,1} \vee P_{2,2} \vee P_{3,1}$

现在首次应用解析规则：R13 中的字面量P2,2 与 R15 中的字面量P2,2 解析，产生解析器。

$R_{16}: \quad P_{1,1} \vee P_{3,1}$

如果坑存在于[1,1]、[2,2]或[3,1]之一中，且不在[2,2]中，则在[1,1]或[3,1]中]。类似地，与 R16 到 R17 中的字面量P1,1 相比，R1 中的字面量P1,1 由 P3,1 解析。

$R_{17}: \quad P_{3,1}$

在英语中，如果一个坑存在于[1,1]或[3,1]中，并且它不在[1,1]中，则它在[3,1]中。单位分辨率推理规则 l1 lk, m 用于最后两个推理阶段。

$\frac{\ell_{1} \vee \cdots \vee \ell_{k}, \quad m}{\ell_{1} \vee \cdots \vee \ell_{i-1} \vee \ell_{i+1} \vee \cdots \vee \ell_{k}}$

其中每个 l 是字面量， l 和 m 是互补字面量（换句话说，否定）。

结果，单元解析规则从一个子句（字面量的析取）和一个字面量创建了一个新的子句。单个字面量，通常称为单元子句，可以理解为一个字面量的析取。

全分辨率规则可以推广到

$\frac{\ell_{1} \vee \cdots \vee \ell_{k}, \quad m_{1} \vee \cdots \vee m_{n}}{\ell_{1} \vee \cdots \vee \ell_{i-1} \vee \ell_{i+1} \vee \cdots \vee \ell_{k} \vee m_{1} \vee \cdots \vee m_{j-1} \vee m_{j+1} \vee \cdots \vee m_{n}}$

在哪里$l_{i}$和$m_{j}$是互补字面量。这意味着当解析两个子句时，将创建一个新子句，其中包含两个原始子句中的所有字面量，除了两个互补的字面量。

$\frac{P_{1,1} \vee P_{3,1}, \quad \neg P_{1,1} \vee \neg P_{2,2}}{P_{3,1} \vee \neg P_{2,2}}$

解析规则还有一个额外的技术特征：每个字面量只能在结果子句中出现一次。分解是删除大量字面量副本的过程。例如，解决$(A \vee B)$和$(A \vee \neg B)$产量$(A \vee A)$ ，可以简化为 A。

考虑字面量$l_{i}$ ，这是对字面量的补充$m_{j}$在另一句话中，确定解决规则的合理性。如果$l_{i}$是真的，那么$m_{j}$是假的，所以$m_{1} \vee \cdots \vee m_{j-1} \vee m_{j+1} \vee \cdots \vee m_{n}$一定是真的，因为$m_{1} \vee \cdots \vee m_{n}$提供。如果$l_{i}$是假的，那么$\ell_{1} \vee \cdots \vee \ell_{k}$必须为真，因为提供了 l1lk。现在，因为 li 可以是真或假，所以这些结论之一必须是真的——正如解决规则所要求的那样。

解析规则更令人吃惊，因为它是一系列完整推理方法的基础。基于分辨率的定理证明器可以确定是否$\alpha \models \beta$在任何陈述的命题逻辑中$\alpha$和$\beta$ .以下两个小节描述了分辨率如何做到这一点。