证明命题定理的证明和推论

本文讨论了如何使用推理规则来创建证明——一系列导致预期结果的结论。最著名的规则被称为Modus Ponens （拉丁语为肯定模式），并表示为

$\frac{\alpha \Rightarrow \beta, \quad \alpha}{\beta}$

证明命题定理的推论

该符号表示只要提供任何该类型的句子，就可以推断出该句子。如果$\text { ( WumpusAhead } \wedge \text { WumpusAlive) } \Rightarrow \text { Shoot }$和$\text { (WumpusAhead } \wedge \text { WumpusAlive) }$两者都提供，Shoot 可以推断。

And-Elimination 是另一个有用的推理规则，它指出任何合取都可以从合取中推断出来：

$\frac{\alpha \wedge \beta}{\alpha}$

WumpusAlive 可以从$\text { (WumpusAhead } \wedge \text { WumpusAlive) }$ ， 例如。通过评估潜在的真值，人们可以很容易地证明 Modus Ponens 和 And-Elimination 是正确的。 $\alpha$和$\beta$ .然后可以将这些原则应用于它们所适用的每种情况，从而得出良好的结论，而无需列举模型。

$\begin{aligned} (\alpha \wedge \beta) & \equiv(\beta \wedge \alpha) \quad \text { commutativity of } \wedge \\ (\alpha \vee \beta) & \equiv(\beta \vee \alpha) \quad \text { commutativity of } \vee \\ ((\alpha \wedge \beta) \wedge \gamma) & \equiv(\alpha \wedge(\beta \wedge \gamma)) \quad \text { associativity of } \wedge \\ ((\alpha \vee \beta) \vee \gamma) & \equiv(\alpha \vee(\beta \vee \gamma)) \quad \text { associativity of } \vee \\ \neg(\neg \alpha) & \equiv \alpha \quad \text { double-negation elimination } \\ (\alpha \Rightarrow \beta) & \equiv(\neg \beta \Rightarrow \neg \alpha) \quad \text { contraposition } \\ (\alpha \Rightarrow \beta) & \equiv(\neg \alpha \vee \beta) \quad \text { implication elimination } \\ (\alpha \Leftrightarrow \beta) & \equiv((\alpha \Rightarrow \beta) \wedge(\beta \Rightarrow \alpha)) \quad \text { biconditional elimination } \\ \neg(\alpha \wedge \beta) & \equiv(\neg \alpha \vee \neg \beta) \quad \text { De Morgan } \\ \neg(\alpha \vee \beta) & \equiv(\neg \alpha \wedge \neg \beta) \quad \text { De Morgan } \\ (\alpha \wedge(\beta \vee \gamma)) & \equiv((\alpha \wedge \beta) \vee(\alpha \wedge \gamma)) \quad \text { distributivity of } \wedge \text { over } \vee \\ (\alpha \vee(\beta \wedge \gamma)) & \equiv((\alpha \vee \beta) \wedge(\alpha \vee \gamma)) \quad \text { distributivity of } \vee \text { over } \wedge \end{aligned}$

上面的等式显示了所有可以用作推理规则的逻辑等价。例如，双条件消除的等价产生了两个推理规则。

$\frac{\alpha \Leftrightarrow \beta}{(\alpha \Rightarrow \beta) \wedge(\beta \Rightarrow \alpha)} \quad \text { and } \quad \frac{(\alpha \Rightarrow \beta) \wedge(\beta \Rightarrow \alpha)}{\alpha \Leftrightarrow \beta}$

一些推理规则不会以相同的方式在两个方向上函数。例如，我们不能反向运行 Modus Ponens 以获得$\alpha \Rightarrow \beta$和$\alpha \text{ from } \beta$ .

让我们看看如何在 wumpus 环境中应用这些等价和推理规则。我们从包括 R1 到 R5 在内的知识库开始，并演示如何建立$\neg P_{1,2}$即[1,2]不包括任何坑。为了生成 R6，我们首先对 R2 应用双条件消除：

$R_{6}: \quad\left(B_{1,1} \Rightarrow\left(P_{1,2} \vee P_{2,1}\right)\right) \wedge\left(\left(P_{1,2} \vee P_{2,1}\right) \Rightarrow B_{1,1}\right)$

之后，我们在 R6 上应用 And-Elimination 得到$R_{7}: \quad\left(\left(P_{1,2} \vee P_{2,1}\right) \Rightarrow B_{1,1}\right)$

对于反例，逻辑等价产生$R_{8}: \quad\left(\neg B_{1,1} \Rightarrow \neg\left(P_{1,2} \vee P_{2,1}\right)\right)$

使用 R8 和感知$R_{4} \text { (i.e., } \neg B_{1,1} \text { ) }$ , 我们现在可以应用 Modus Ponens 得到$R_{9}: \quad \neg\left(P_{1,2} \vee P_{2,1}\right)$ .

最后，我们使用德摩根规则得出以下结论： $R_{10}: \quad \neg P_{1,2} \wedge \neg P_{2,1}$

也就是说[1,2]和[2,1]都没有坑。

我们手动找到了这个证明，但是任何搜索技术都可以用来生成类似证明的步骤序列。我们现在要做的就是定义一个证明问题：

• 初始状态：知识的起点。
• 动作：动作集合由已应用于符合推理规则上半部分的所有句子的所有推理规则组成。
• 结果：将语句添加到推理规则的底部是操作的结果。
• 目标：目标是达到包含我们试图验证的短语的状态。

因此，寻找证明是计算模型的可行替代方案。