归结演绎推理：基于鲁滨逊原理的机器推理技术

归结演绎推理是一种基于鲁滨逊归结原理的机器推理技术。

（一）子句集及其化简

采用归结演绎推理方法，其问题是用谓词公式表示的，其推理则是在子句集的基础上进行的，因此在讨论该方法之前，需要先介绍子句集的有关概念及化简方法。

1.子句和子句集

定义3－1：原子谓词公式及其否定统称为文字。

例如，P（x），Q（x），┐P（x），┐Q（x）等都是文字。

定义3－2：任何文字的析取式称为子句。

例如，P（x）∨Q（x），P（x，f（x））∨Q（x，g（x））都是子句。

定义3－3：不包含任何文字的子句称为空子句。

由于空子句不含有任何文字，也就不能被任何解释所满足，因此空子句是永假的，不可满足的。空子句一般被记为□或NIL。

定义3－4：由子句或空子句所构成的集合称为子句集。

2.子句集的化简

在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理规则将其转化成相应的子句集。其化简步骤如下：

（1）消去连接词“→”和“↔”

反复使用如下等价公式

即可消去谓词公式中的连接词“→”和“↔”。

如公式（∀x）（（∀y）P（x，y）→┐（∀y）（Q（x，y）→R（x，y））经等价变化后为

（2）减少否定符号的辖域

将每个否定符号“┐”移到紧靠谓词的位置，使得每个否定符号最多只作用于一个谓词上。

例如，上步所得公式经本步变换后为

（3）对变元标准化

在一个量词的辖域内，把谓词公式中受该量词约束的变元全部用另一个没有出现过的任意变元代替，使不同量词约束的变元有不同的名字。

例如，上步所得公式经本步变换后为

（4）化为前束范式

化为前束范式的方法是把所有量词都移到公式的左边，并且在移动时不能改变其相对顺序。由于第③步已对变元进行了标准化，每个量词都有自己的变元，这就消除了任何由变元引起冲突的可能，因此这种移动是可行的。

例如，上步所得公式化为前束范式后为

（5）消去存在量词

消去存在量词时，需要区分以下两种情况。

若存在量词不出现在全称量词的辖域内（即它的左边没有全称量词），只要用一个新的个体常量替换受该存在量词约束的变元，就可消去该存在量词。(www.xing528.com)

若存在量词位于一个或多个全称量词的辖域内，如则需要用Skolem函数f（x1，x2，…，xn）替换受该存在量词约束的变元，再消去该存在量词。

（6）化为Skolem标准形

Skolem标准形的一般形式为

式中，M（x1，x2，…，xn）是Skolem标准形的母式，由子句的合取构成。

把谓词公式化为Skolem标准形需要使用以下等价关系

例如，上步所得的公式化为Skolem标准形后为

（7）消去全称量词

由于母式中的全部变元均受全称量词的约束，并且全称量词的次序已无关紧要，因此可以省掉全称量词。但剩下的母式仍假设其变元是被全称量词量化的。

例如，上步所得公式消去全称量词后为

（8）消去合取词

在母式中消去所有合取词，把母式用子句集的形式表示出来。其中，子句集中的每个元素都是一个子句。

例如，上步所得公式的子句集中包含以下两个子句

（9）更换变元名称

对子句集中的某些变元重新命名，使任意两个子句中不出现相同的变元名。由于每一个子句都对应着母式中的一个合取元，并且所有变元都是由全称量词量化的，因此任意两个不同子句的变元之间实际上不存在任何关系。这样，更换变元名是不会影响公式的真值的。

例如，对上步所得公式，可把第二个子句集中的变元名x更换为y，得到如下子句集

（二）鲁滨逊归结原理

鲁滨逊归结原理也称为消解原理，是鲁滨逊（Robinson）于1965年在海伯伦（Herbrand）理论的基础上提出的一种基于逻辑“反证法”的机械化定理证明方法。其基本思想是把永真性的证明转化为不可满足性的证明，即要证明P→Q永真，只要能够证明P∧┐Q为不可满足即可。

鲁宾逊归结原理可分为命题逻辑归结原理和谓词逻辑归结原理。

（三）归结演绎推理的方法

1.命题逻辑的归结演绎推理

应用归结原理证明定理的过程称为归结反演。在命题逻辑中，已知F，证明G为真的归结反演过程如下：

①否定目标公式G，得┐G。

②把┐G并入到公式集F中，得到{F，┐G}。

③把{F，┐G}化为子句集S。

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

2.谓词逻辑的归结演绎推理

谓词逻辑的归结反演过程与命题逻辑的归结反演过程相比，其步骤基本相同，但每步的处理对象不同。