人工智能 —— 归结演绎推理 - 好文

<>什么是归结演绎推理

*
归结演绎推理是一种基于逻辑“反证法”的机械化定理证明方法。其基本思想是把永真性的证明转化为不可满足性的证明。即要证明 P→QP→QP→Q 永真，只要能够证明
P∧﹁QP∧﹁QP∧﹁Q 为不可满足即可。

*
谓词公式不可满足的充要条件是其子句集不可满足。因此，要把谓词公式转换为子句集，再用鲁滨逊归结原理求解子句集是否不可满足。如果子句集不可满足，则 P→QP→QP
→Q 永真

<>逻辑学基础

（1）谓词公式的永真性

如果谓词公式P对非空个体域D上的任一解释都取得真值T，则称P在D上是永真的；如果P在任何非空个体域上均是永真的，则称P永真。

（2）谓词公式的可满足性

对于谓词公式P，如果至少存在D上的一个解释，使公式P在此解释下的真值为T，则称公式P在D上是可满足的。

（3）谓词公式的范式

范式是公式的标准形式，公式往往需要变换为同它等价的范式，以便对它们进行一般性的处理。在谓词逻辑中，根据量词在公式中出现的情况，可将谓词公式的范式分为以下两种。

前束范式

* 任一含有量词的谓词公式均可化为与其对应的前束范式

Skolem 范式

* 任一含有量词的谓词公式均可化为与其对应的Skolem范式

<>子句和子句集

<>谓词公式化为子句集

<>鲁滨逊归结原理（消解原理）

基本思想：

* 检查子句集S中是否包含空子句，若包含，则S不可满足。
* 若不包含，在S中选择合适的子句进行归结，一旦归结出空子句，就说明S是不可满足的。
（1）命题逻辑中的归结原理：

设 C1C_1C1 与 C2C_2C2 是子句集中的任意两个子句，如果 C1C_1C1 中的文字 L1L_1L1 与 C2C_2C2 中的文字 L2
L_2L2 互补，那么从 C1C_1C1 和 C2C_2C2 中分别消去 L1L_1L1 和 L2L_2L2
，并将二个子句中余下的部分析取，构成一个新子句C12C_{12}C12 。其中，C12C_{12}C12 称为 C1C_1C1 和 C2C_2C2
的归结式，C1C_1C1 和 C2C_2C2 称为 C12C_{12}C12 的亲本子句。

（2）谓词逻辑中的归结原理：

设 C1C_1C1 和 C2C_2C2 是两个没有公共变元的子句， L1L_1L1 和 L2L_2L2 分别是 C1C_1C1 和 C2C_2C2
中的文字。如果L1L_1L1 和 L2L_2L2 存在最一般合一 σσσ，则称 C12=(C1σ−L1σ）U（C2σ−L2σ)
C_{12}=({C_1σ}-{L_1σ}）U（{C_2σ}-{L_2σ})C12=(C1σ−L1σ）U（C2σ−L2σ) 为 C1C_1C1 和
C2C_2C2 的二元归结式，而 L1L_1L1 和 L2L_2L2 为归结式上的文字。

<>归结反演

（1）归结反演证明定理：

步骤：

（1）将已知前提表示为谓词公式 FFF。

（2）将待证明的结论表示为谓词公式 QQQ，并否定得到﹁Q﹁Q﹁Q。

（3）把谓词公式集 {F,﹁Q}\{F,﹁Q\}{F,﹁Q} 化为子句集 SSS。

（4）应用归结原理对子句集 SSS 中的子句进行归结，并把每次归结得到的归结式都并入到 SSS 中。如此反复进行，若出现了空子句，则停止归结，此时就证明了 Q
QQ 为真。

（2）归结反演求解问题：

步骤：

（1）已知前提 FFF 用谓词公式表示；

（2）把待求解的问题 QQQ 用谓词公式表示，并否定 QQQ ，再与 ANSWERANSWERANSWER 构成析取式（﹁Q∨ANSWER）（﹁Q
∨ANSWER）（﹁Q∨ANSWER）

（3）把谓词公式集 {F,（﹁Q∨ANSWER）}\{F,（﹁Q ∨ANSWER）\}{F,（﹁Q∨ANSWER）} 化为子句集 SSS。

（4）对 SSS 应用归结原理进行归结；

（5）若得到归结式 ANSWERANSWERANSWER ，则答案就在 ANSWERANSWERANSWER 中。

<>归结演绎推理的应用

（1）归结反演证明定理：

（2）归结反演求解问题：

热门工具换一换