归结反演

        概述

    归结反演就是用归结反演的方法实现定理的证明。设有一个公式集S，希望从 S证明某个目标公式W，证明方法如下：

    （1）将ØW加入到集合S 。

    （2）将新的S集合转换成一组子句，应用归结原理推导出一个空子句。

     显然，由与{P}和{ØP}类似的子句才能推导出空子句，因此空子句可看作是一个矛盾。由集合S∨{ØW}推导出空子句说明集合S和公式ØW是矛盾的。满足集合S的每一个解释都不会满足公式ØW。也就是说，没有一个解释能满足集合S和{ØW}的并集，因此集合S∪{ØW}是不可满足的。集合S与公式ØW的矛盾，证明公式W逻辑上是遵从集合S的。

　  下一页我们从一个简单的例子来学习归结反