归结推理规则及其在虚拟现实与人工智能应用技术中的融合性研究

归结证明过程是一种反驳程序，即不是证明一个公式有效，而是证明公式之非是不一致的。这完全是为了方便，并且不失一般性。归结推理规则所应用的对象是命题或谓词合式公式的一种特殊的形式，称为子句。因此，在使用归结推理规则进行归结之前需要把合式公式化为子句式。

在数理逻辑中，我们知道如何把一个公式化成前束标准型（Q1x1）…（Qnxn）M，由于M中不含量词，因此总可以把它变换成合取范式。无论是前束标准型还是合取范式都与原来的合式公式等值。

对于前束范式

其中，表示M中含有变量元，并且M是合取标准型。使用下述方法，可以消去前缀中的所有存在量词：

令　Qr是（Q1x1）…（Qnxn）中出现的存在量词（1≤r≤n）。(www.xing528.com)

（1）若在Qr之前不出现全称量词，则选择一个与M中出现的所有常量都不相同的新常量c，用c代替M中出现的所有xr，并且由前缀中删去（Qrxr）。

（2）若Qs1，…，Qsm是在Qr之前出现的所有全称量词（1≤s1≤s2≤...≤sm＜r），则选择一个与M中出现的任一函数符号都不相同的新m元函数符号f，用f（xs1，...xsm）其中s1，sm的为下标代替M中的所有xr，并且由前缀中删去（Qrxr）。

按上述方法删去前缀中的所有存在量词之后得出的公式称为合式公式的Skolem标准型。替代存在量化变量的常量c（视为0元函数）和函数f称为Skolem函数。

归结反演不仅可以用于定理证明，而且可以用来求取问题的答案，其思想与定理证明类似。方法是在目标公式的否定形式中加上该公式否定的否定，得到重言式；或者再定义一个新的谓词ANS ，加到目标公式的否定中，把新形成的子句加到子句集中进行归结。