命题逻辑的推理模式

7.5 命题逻辑的推理模式

本节论述推理的标准模式，它可用于生成导致期望目标的结论链。这些推理模式被称为推理规则。最著名的规则是分离规则（Modus Ponens），书写如下：

此符号的意思是，只要给定任何形式为αβ的语句和α，就可以推导出语句β。例如，如果已知(WumpusAhead∧WumpsAlive)  Shoot和(WumpusAhead∧WumpsAlive)，那么可以推导出Shoot。

另一个有用的推理规则是与消去，也就是说，可以从一个合取式推导出任何合取子句：

例如，从WumpusAhead∧WumpsAlive可以推导出WumpusAlive。

通过考虑α 和β 的可能真值，很容易看出，分离规则和与消去都是永远可靠的。于是这些规则可以用于它们适用的任意特定实例，生成可靠的推理而无需对模型进行枚举。

图7.11中的所有逻辑等价都可以作为推理规则。例如，用于双向蕴涵消去的等价给出两条推理规则：

不是所有的推理规则可以像这个规则一样两个方向都生效。例如，我们无法按相反方向运用分离规则（ModusPonens），从β得到αβ和α 。

让我们看看这些推理规则和等价如何应用于 wumpus 世界。我们从包含 R1到 R5的知识库开始，并说明如何证明¬P1,2，也就是说，证明[1, 2]中没有陷阱。首先，将双向蕴涵消去应用于R2，得到

接着，对R6进行与消去，得到

其逆否命题的逻辑等价给出

现在，我们可以对R8和感知信息R4（也就是¬B1,1）运用分离规则，得到

R9:　　 ¬(P1,2∨P2,1)

最后，我们应用摩根律，给出结论

R10:　　 ¬P1,2∧¬P2,1

也就是说，[1, 2]和[2, 1]二者都不包含陷阱。

前述的推导过程——推理规则的应用序列——称为一个证明。寻找证明的过程与搜索问题中寻找解的过程非常类似。实际上，如果定义后继函数以便生成推理规则所有可能的应用，那么第三章和第四章中的所有搜索算法可以用于寻找证明。因而，搜索证明是模型枚举的一个替换方法。搜索过程可以从最初的知识库正向出发，应用推理规则以生成目标语句，或者从目标语句反向进行，试图找到由初始知识库引出的推理规则链。本节的后面部分，我们将给出分别采用这些技术的两个算法家族。

命题逻辑的推理是 NP 完全的，这个事实表明最坏的情况下，搜索证明的方法将不比模型的枚举方法更有效率。然而，在很多实际情况中，寻找某个证明的过程可以高效简单，因为无论存在多少命题，它都可以忽略不相干命题。例如，先前给出的可以推导出¬P1,2∧¬P2,1的证明没有提及命题B2,1、P1,1、P2,2或P3,1。它们可以被忽略的原因在于，目标命题P1,2只在语句R4中出现；R4中的其它命题只在R2和R4中出现；因此，R1、R3和R5与证明过程无关。即便我们把上百万的更多语句添加到知识库，最后结果还是相同的；另一方面，简单的真值表算法将会由于模型的指数爆炸而失效。

逻辑系统的这一特征本质上遵循一个更基本的、被称为单调性的概念。单调性意味着蕴涵语句集在信息被添加到知识库的时候只会增长[11]。对于任意语句α 和β ，

如果 KB|= α ，那么KB∧β|= α

例如，假设知识库包含附加断言β ，β 宣称世界中正好有8个陷阱。这条知识将有助于智能体提取出附加结论，但是它无法使得任意已经推导出的结论α 无效——诸如[1, 2]中没有陷阱的结论。单调性意味着任何时刻只要在知识库中发现了合适的前提，就可以应用推理规则——规则的结论一定遵循“与知识库中的其余内容无关”的要求。