Herbrand定理的一个改进及其在模型生成定理证明法中的应用
An Improvement of Herbrands Theorem and Its Application to Model Generation Theorem Proving
-
摘要: Herbrand定理是绝大多数一阶谓词论理的自动推理（定理证明）方法的理论基础。根据 Herbrand定理，对于任意给定的句集合S，可以机械地定义一个与S相对应的特殊的领域，即所谓的Herbrand领域（在很多情况下是无限的）。如果C是句集合S中的一个论理句，那么将C中的所有的变量用Herbrand领域的要素替代后所生成的结果被称为C的基本句。Herbrand定理指出，对于一个给定的句集合S，当而且仅当存在着一个不能满足的S的（矛盾的）基本句集合时， S才是不能满足的。 Herbrand定理给出了一个机械式地进行一阶谓词论理的自动推理（定理证明）的方法。对于一个给定的句集合S，我们可以从零集合T开始，不断地往T里加入S的基本句，并用命题论理的方法判断其是否不能满足。如果S是不能满足的，我们一定可以用这种方法找到一个不能满足的T。由于在通常的情况下，基本句的数量很大（在很多情况下有无限个），所以直接使用 Herbrand定理进行自动推理（定理证明）的效果并不好，因为有许多的基本句不仅与我们的推理无关，而且会引起不必要的推论。 也正因为如此，人们提出了各种有效的方法来选择或限制用于自动推理的基本句。 如果能减少需要考虑的基本句的数量，就能提高自动推理的效率。基于这个出发点， 本论文对 Herbrand定理提出了一点改进。对于一个给定的句集合S，不同于只建立一个标准的Herbrand领域，我们为S中的每一个谓词及函数的参数建立一个Herbrand领域的子集，并证明当而且仅当存在着一个将S中的变量用对应于该变量的Herbrand领域的子集的要素替代后所生成的不能满足的基本句集合时，S才是不能满足的。由于对应于参数的Herbrand领域的子集一般都小于标准的Herbrand领域（有时是有限和无限之差），所以需要考虑的基本句的数量也会相应地减少，从而达到提高自动推理的效率的目的。 作为一个应用，我们将其用于提高正向推理定理证明（Foward Chaining Theorem Proving）中对于非领域限制问题的效率问题。非领域限制问题是指给定的句集合中，存在着这样的论理句，它的结论中含有不存在于前提中的变量（这样的变量被称为非领域限制变量）。正向推理定理证明是一种只适用于领域限制问题的推论方法。非领域限制问题可以转换为具有等同意义的领域限制问题，但非领域限制变量会被泛化到整个Herbrand领域，生成大量的可能与推论无关的基本句，从而严重地影响到推论的效率。根据我们对 Herbrand定理的改进，在将非领域限制问题转换为领域限制问题时，我们可以将非领域限制变量的取值限制在与其对应的Herbrand领域的子集上，从而减少生成的基本句，使推论效率得以提高。我们给出这样的转换算法，并通过实验对其有效性进行了验证。Abstract: This paper presents an improvement of Herbrand's theorem. We propose a method for specifying a sub-universe of the Herbrand universe of a clause set \cal S for each argument of predicate symbols and function symbols in \cal S. We prove that a clause set \cal S is unsatisfiable if and only if there is a finite unsatisfiable set of ground instances of clauses of \cal S that are derived by only instantiating each variable, which appears as an argument of predicate symbols or function symbols, in \cal S over its corresponding argument's sub-universe of the Herbrand universe of \cal S. Because such sub-universes are usually smaller (sometimes considerably) than the Herbrand universe of \cal S, the number of ground instances may decrease considerably in many cases. We present an algorithm for automatically deriving the sub-universes for arguments in a given clause set, and show the correctness of our improvement. Moreover, we introduce an application of our approach to model generation theorem proving for non-range-restricted problems, show the range-restriction transformation algorithm based on our improvement and provide examples on benchmark problems to demonstrate the power of our approach.
下载: