论文部分内容阅读
[摘要]归结原理使用较广，是定理机器证明的理论基础。既可以用来证明一些目标公式和逻辑结论的成立，又可以用来求解应用问题的答案。比如一个目标公式 xW（x），有时我们不但要求证明它成立，而且希望知道变元x的一个例，即如果回答x=A，W是否为真？可直接用归结反演证明，但要回答x=? W为真时，就需要问题的答案。本文给出了归结原理在这两方面的应用，最后指出了使用水平浸透法证明不可满足性所带来的子句冗余，以及避免子句冗余的一个方法。
[关键词]归结原理；人工智能；机器证明；水平浸透法
自动定理证明是人工智能科学中的一个重要的研究领域，许多数学问题甚至是非数学问题（如医疗诊断，机器人行动规划）都可以归结为一个定理证明的问题。在定理机器证明中，已知一公式集F1，F2…Fn，要证明一个公式W是否成立，即要证明W是公式集的逻辑推论时，一种方法是要证明F1∧F2∧…∧Fn→W为永真，如果直接运用推理规则进行推导，由于演绎技巧等因素，给建立机器证明系统带来困难。另一种证明方法是采用间接法（反证法），即不去证明F1∧F2∧…∧Fn→W为真，而是去证明F=F1∧F2∧…∧Fn∧~W为永假，这就等价于证明F对应的子句集S=S0∨｛~W｝为不可满足的。这时候如果用归结作为推理规则使用时，就可以使机器证明简化了。
归结原理的思想是设法检验扩充的子句集S1是否有空子句。若S中有空子句，则S为不可满足的，若没有空子句，就进一步用归结法从S导出S1，然后再检验S1是否有空子句，可以证明用归结法导出的扩大子句集S1，其不可满足性是不变的，所以S1中有空子句，也就证明了S的不可满足性。归结过程可以一直进行下去，就是要通过归结过程演绎出S的不可满足性来，从而使定理得到证明。
一、基本原理
对于子句集S中的任意两个子句C1，C2，若在C1中有一个文字L1，它是子句C2中文字L2的补，那么从C1，C2中分别消去L1和L2，并将剩下的子句构成析取，这样的新子句称为C1，C2的归结式。
定理：设两个子句C1，C2，它们的归结式是C12，则C12是C1和C2的有效逻辑推论。
推论：子句集S=｛C1，C2，…，Cn｝与子句集S1=｛C，C1，C2…，Cn｝的不可满足性是相同的S1中的C是C1，C2的归结式，即S1是对S应用归结法后导出的子句集。
二、归结过程
对于公理集F和命题P，则归结过程如下：
（1）把F转化为子句集形式，得到子句集S0。
（2）把命题的否定也转化为子句集表示，并加入到S0中，得S=S0∨｛S~p｝。
（3）对子句集反复使用归结规则，直到导出含有空子句的子句集为止。即出现归结式为空子句情况是，表明矛盾产生，证明结束。
（4）对有需要的地方分别使用替换或合一替换规则。
下面以例子来说明上述思想。
例：（1）会朗读的人是识字的（2）海豚都不识字（3）有些还豚是很机灵的
求证：有些机灵的东西不会朗读。
证明：首先把上述知识用谓词逻辑对应表示如下：
（1）x（R（x）→L（x））
（2）x（D（x）→~ L（x））
（3）x（D（x） ∧I（x））
目标公式表示为： x（I（x）∧ ~ R（x））
然后将（1）（2）（3）化为如下的子句集：
1. ~R（x） ∨ L（x）
2. ~D（y）∨ ~ L（y）
3.D（A）
4.I（A）
目标公式的否定化为子句集
5.~I（w）∨R（w）
归结过程如下：
6. R（A） 4、5
7.L（A）6、1
8. ~D（A）7、2
9. NIL 8、3
故得证。
上述的反演一般可以用来证明目标公式的成立，但如果含有存在量词量化变元的目标公式，如 xW（x），有时我们不但要求证明它成立，而且希望知道变元X的一个例，可以直接用反演法证明，但要回答X=？W为真，就需要问题的答案。这种问题的解答步骤如下：
（1）把已知前提的谓词公式化为相应的子句集，设为S
（2）把待求解的问题也用谓词公式表示出来，然后把它否定
（3）设一个ANSWER谓词，其变元与问题公式的变元完全相同，把它与（2）析取，并化为子句集，然后把它并入S中。
（4）对S应用归结原理进行归结。
（5）若得到的归结式是ANSWER，则答案就在ANSWER中。
例已知：王先生是小李的老师，小李是小张的同班同学，如果X与Y是同班同学，则X的老师也是Y 的老师。
求：小张的老师是谁？
解：T（x，y）:x 是y的老师
C（x，y）x 是y的同学
则根据上述条件有：（1）T（wang ，li）；
（2） C （li ，zhang）；
（3）x y z（C（x，y） ∧T（z，x）→T（z，y））
（4） ~ xT（x，zhang）∨ANSWER（x）
把上述化为子句S有：
（1）T （wang ，li）
（2） C （li ，zhang）；
（3） ~C（x，y）∨ ~ T（z，x） ∨T（z，y）
（4） ~T（u，zhang） ∨ANSWER（wang）
对上述子句集进行归结有：
（5） ~C（li，y） ∨T（wang，y）（1）（3）
（6） ~C（li，zhang） ∨ANSWER（wang）（4）（5）
（7） ANSWER（wang） （2）（6）
所以得出结论：小张的老师是王老师。
上述例子都是基于水平浸透法的归结证明，会产生大量不相干的和多余的子句，再如下例：
令S=｛~P∨~Q∨R，P∨R，Q∨R，~R｝。用水平浸透法证明S的不可满足性，过程如下：S0： （1）~P∨~Q∨R
（2）P∨R
（3）Q∨R
（4）~R
S1：（5）~Q∨R（1），（2）
（6）~P∨R（1），（3）
（7）~P∨~Q （1），（4）
（8）P（2），（4）
（9）Q（3），（4）
S2：（10）~Q∨R（删除） （1），（8）
（11）~P∨R（删除） （1），（9）
（12）R （2），（6）
（13）~Q∨R（删除） （2），（7）
（14）R（删除） （3），（5）
（15）~Q（4），（5）
（16）~P（4），（6）
（17）R（删除） （5），（9）
（18）R（删除） （6），（8）
（19）~Q（删除）（7），（8）
（20）~P（删除）（7），（9）
（21）R（删除） （2），（16）
（22）R（删除） （3），（15）
（23）□（4），（12）
可以看出，在整个证明过程中，有用的子句只有（6）和（12），其他子句都是不相干的和多余的。如果用某种方法将子句集S分成两部分，S1和S2，并且同一集合里的子句不允许进行归结，那就能阻止很多子句的产生，当然条件是不能阻止空子句的产生。在上面的例子里，如果将S分为：
S1=｛（2），（3）｝，S2=｛（1），（4）｝
则就阻止了（1）和（4）进行的归结，但是（2），（3）仍然能和（4）归结。如果我们也能阻止（2），（3）和（4）的归结，则在S1中就只剩下子句（5），（6），阻止了子句（7），（8），（9）的产生。
[参考文献]
[1] 王宪钧.数理逻辑引论〔M〕.北京：北京大学出版社，1988.
[2] 何华灿.人工智能导论〔M〕.西安：西北工业大学出版社，1988.
[关键词]归结原理；人工智能；机器证明；水平浸透法
自动定理证明是人工智能科学中的一个重要的研究领域，许多数学问题甚至是非数学问题（如医疗诊断，机器人行动规划）都可以归结为一个定理证明的问题。在定理机器证明中，已知一公式集F1，F2…Fn，要证明一个公式W是否成立，即要证明W是公式集的逻辑推论时，一种方法是要证明F1∧F2∧…∧Fn→W为永真，如果直接运用推理规则进行推导，由于演绎技巧等因素，给建立机器证明系统带来困难。另一种证明方法是采用间接法（反证法），即不去证明F1∧F2∧…∧Fn→W为真，而是去证明F=F1∧F2∧…∧Fn∧~W为永假，这就等价于证明F对应的子句集S=S0∨｛~W｝为不可满足的。这时候如果用归结作为推理规则使用时，就可以使机器证明简化了。
归结原理的思想是设法检验扩充的子句集S1是否有空子句。若S中有空子句，则S为不可满足的，若没有空子句，就进一步用归结法从S导出S1，然后再检验S1是否有空子句，可以证明用归结法导出的扩大子句集S1，其不可满足性是不变的，所以S1中有空子句，也就证明了S的不可满足性。归结过程可以一直进行下去，就是要通过归结过程演绎出S的不可满足性来，从而使定理得到证明。
一、基本原理
对于子句集S中的任意两个子句C1，C2，若在C1中有一个文字L1，它是子句C2中文字L2的补，那么从C1，C2中分别消去L1和L2，并将剩下的子句构成析取，这样的新子句称为C1，C2的归结式。
定理：设两个子句C1，C2，它们的归结式是C12，则C12是C1和C2的有效逻辑推论。
推论：子句集S=｛C1，C2，…，Cn｝与子句集S1=｛C，C1，C2…，Cn｝的不可满足性是相同的S1中的C是C1，C2的归结式，即S1是对S应用归结法后导出的子句集。
二、归结过程
对于公理集F和命题P，则归结过程如下：
（1）把F转化为子句集形式，得到子句集S0。
（2）把命题的否定也转化为子句集表示，并加入到S0中，得S=S0∨｛S~p｝。
（3）对子句集反复使用归结规则，直到导出含有空子句的子句集为止。即出现归结式为空子句情况是，表明矛盾产生，证明结束。
（4）对有需要的地方分别使用替换或合一替换规则。
下面以例子来说明上述思想。
例：（1）会朗读的人是识字的（2）海豚都不识字（3）有些还豚是很机灵的
求证：有些机灵的东西不会朗读。
证明：首先把上述知识用谓词逻辑对应表示如下：
（1）x（R（x）→L（x））
（2）x（D（x）→~ L（x））
（3）x（D（x） ∧I（x））
目标公式表示为： x（I（x）∧ ~ R（x））
然后将（1）（2）（3）化为如下的子句集：
1. ~R（x） ∨ L（x）
2. ~D（y）∨ ~ L（y）
3.D（A）
4.I（A）
目标公式的否定化为子句集
5.~I（w）∨R（w）
归结过程如下：
6. R（A） 4、5
7.L（A）6、1
8. ~D（A）7、2
9. NIL 8、3
故得证。
上述的反演一般可以用来证明目标公式的成立，但如果含有存在量词量化变元的目标公式，如 xW（x），有时我们不但要求证明它成立，而且希望知道变元X的一个例，可以直接用反演法证明，但要回答X=？W为真，就需要问题的答案。这种问题的解答步骤如下：
（1）把已知前提的谓词公式化为相应的子句集，设为S
（2）把待求解的问题也用谓词公式表示出来，然后把它否定
（3）设一个ANSWER谓词，其变元与问题公式的变元完全相同，把它与（2）析取，并化为子句集，然后把它并入S中。
（4）对S应用归结原理进行归结。
（5）若得到的归结式是ANSWER，则答案就在ANSWER中。
例已知：王先生是小李的老师，小李是小张的同班同学，如果X与Y是同班同学，则X的老师也是Y 的老师。
求：小张的老师是谁？
解：T（x，y）:x 是y的老师
C（x，y）x 是y的同学
则根据上述条件有：（1）T（wang ，li）；
（2） C （li ，zhang）；
（3）x y z（C（x，y） ∧T（z，x）→T（z，y））
（4） ~ xT（x，zhang）∨ANSWER（x）
把上述化为子句S有：
（1）T （wang ，li）
（2） C （li ，zhang）；
（3） ~C（x，y）∨ ~ T（z，x） ∨T（z，y）
（4） ~T（u，zhang） ∨ANSWER（wang）
对上述子句集进行归结有：
（5） ~C（li，y） ∨T（wang，y）（1）（3）
（6） ~C（li，zhang） ∨ANSWER（wang）（4）（5）
（7） ANSWER（wang） （2）（6）
所以得出结论：小张的老师是王老师。
上述例子都是基于水平浸透法的归结证明，会产生大量不相干的和多余的子句，再如下例：
令S=｛~P∨~Q∨R，P∨R，Q∨R，~R｝。用水平浸透法证明S的不可满足性，过程如下：S0： （1）~P∨~Q∨R
（2）P∨R
（3）Q∨R
（4）~R
S1：（5）~Q∨R（1），（2）
（6）~P∨R（1），（3）
（7）~P∨~Q （1），（4）
（8）P（2），（4）
（9）Q（3），（4）
S2：（10）~Q∨R（删除） （1），（8）
（11）~P∨R（删除） （1），（9）
（12）R （2），（6）
（13）~Q∨R（删除） （2），（7）
（14）R（删除） （3），（5）
（15）~Q（4），（5）
（16）~P（4），（6）
（17）R（删除） （5），（9）
（18）R（删除） （6），（8）
（19）~Q（删除）（7），（8）
（20）~P（删除）（7），（9）
（21）R（删除） （2），（16）
（22）R（删除） （3），（15）
（23）□（4），（12）
可以看出，在整个证明过程中，有用的子句只有（6）和（12），其他子句都是不相干的和多余的。如果用某种方法将子句集S分成两部分，S1和S2，并且同一集合里的子句不允许进行归结，那就能阻止很多子句的产生，当然条件是不能阻止空子句的产生。在上面的例子里，如果将S分为：
S1=｛（2），（3）｝，S2=｛（1），（4）｝
则就阻止了（1）和（4）进行的归结，但是（2），（3）仍然能和（4）归结。如果我们也能阻止（2），（3）和（4）的归结，则在S1中就只剩下子句（5），（6），阻止了子句（7），（8），（9）的产生。
[参考文献]
[1] 王宪钧.数理逻辑引论〔M〕.北京：北京大学出版社，1988.
[2] 何华灿.人工智能导论〔M〕.西安：西北工业大学出版社，1988.