4.3 归结反演系统（Refutation）

　　1．归结反演产生式系统的基本算法

　　归结方法的基本算法很简单，每次从子句集中选择两个可进行归结的子句，求它们的归结式，如果归结式为NIL，则算法结束，结论得证。如果归结式不为空，则将该归结式加入到子句集中，继续以上过程。
　　也许你已经注意到了，当归结出空子句NIL时，说明结论是正确的，此时算法结束。但是算法并没有说明什么情况下结论不正确。或者说，如果不能证明结论正确时，算法何时结束。
　　事实上在一阶谓词逻辑的范围内，这一点是做不到的。已经证明，在给定的已知条件下，如果结论成立，则归结法可以在有限的步数内证明该结论成立。但是如果在给定的条件下，结论不成立，则不存在一个通用的方法，可以在有限的步骤内证明该结论不成立。

可以把不断进行归结反演的证明过程用产生式系统进行求解，这时产生式系统的描述及算法为：
综合数据库：子句集

　　2．搜索策略

　　归结方法很简单，但是即便是对于一个比较简单的问题，往往可以进行归结的子句也比较多。如何从众多的可归结的子句中选择两个子句，即为搜索策略问题。不同的搜索策略，会影响到系统的效率和开销，同时也会涉及到完备性问题。当给定的问题在已知条件下成立时，如果某种归结策略一定可以在有限步内证明问题是成立的，则该策略是完备的，否则则是不完备的。这里介绍的是几种在归结过程中常用的搜索策略。这些策略中有些是完备的，有些是非完备的，应该注意每种策略的完备性。在系统实现时，我们当然希望选择完备的搜索策略，但一些非完备的搜索策略往往具有较高的求解效率，因此也有使用的必要性。

　　搜索策略的主要任务是在算法的第4步中选哪两个子句做归结，以及在第5步决定这两个子句中对哪一个文字做归结。在介绍几个实用的策略之前，我们先通过例子讨论该产生式系统具有可交换性的特点以及搜索策略的目标问题。
　　现在我们用产生式系统来求解上一节所举的例子。我们已经得到一个基本的子句集

若用一般的宽度优先图搜索策略求解，其部分搜索图如图4.2所示。由图可以看出，该系统满足可交换系统的性质，因此可用最简单的不可撤回的策略求解，总能找到一个证明解。即当求解过程选用了某条无用的规则之后，不必考虑回溯，也不必顾及规则顺序，只要使用了若干适当的规则之后，就必定会找到解路径。
　　实际上归结过程用归结反演树表示比较简单，图4.3给出上例的一棵归结反演树。搜索策略的目标就是要找到一棵归结反演树。一个反演系统当存在一个矛盾时，如果使用的一种策略，最终都将找到一棵反演树（即能找到矛盾），则这种策略是完备的。在实际应用中，有些策略虽不完备，但具有极高的效率，也是可取的。提高策略效率的一些作法是：只归结含有互补对的文字；及时删去出现的重言式和被其他子句所包含的子句；每次归结都取与目标公式否定式有关的子句作为母子句之一进行归结等等。下面仅对典型的几种策略做一些简单的讨论。