人工智能原理教案02章 归结推理方法2.6 Herbrand定理.doc

2.6 Herbrand定理Herbrand定理是归结原理的理论基础，归结原理的正确性是通过Herbrand定理来证明的。同时归结原理是Herbrand定理的具体实现，利用Herbrand定理对公式的证明是通过归结法来进行的。本节简单地描述了Herbrand定理的基本思想和相关预备知识，最后给出Herbrand定理的一般形式。 公式G永真：对于G的所有解释，G都为真。公式G永假（矛盾）： 没有一个解释使G为真。2.6.1 Herbrand 定理概述问题：一阶逻辑公式的永真性（永假性）的判定是否能在有限步内完成？1936年图灵(Turing)和邱吉(Church)互相独立地证明了：没有一般的方法使得在有限步内判定一阶逻辑的公式是否是永真（或永假）。但是如果公式本身是永真（或永假）的，那么就能在有限步内判定它是永真（或永假）。对于非永真（或永假）的公式就不一定能在有限步内得到结论。判定的过程将可能是不停止的。2.6.1.1 Herbrand 定理思想要证明一个公式是永假的，采用反证法的思想（归结原理），就是要寻找一个已给的公式是真的解释。然而，如果所给定的公式的确是永假的，就没有这样的解释存在，并且算法在有限步内停止。因为量词是任意的，所讨论的个体变量域D是任意的，所以解释的个数是无限、不可数的，要找到所有的解释是不可能的。Herbrand 定理的基本思想是简化讨论域，建立一个比较简单、特殊的域，使得只要在这个论域上（此域称为H域），原谓词公式仍是不可满足的，即保证不可满足的性质不变。H域和D域关系的如下图表示：图21 H域与D域关系示意图t2-1_swf.htm2.6.1.2 H域H域的定义：设S为给定公式G的子句集，定义在论域D上，H0为S中的常量集。如果S中没有常量，H0由任意单个常量构成，如a，Hi+1= Hifm(t1, t2, tn), i=0, 1, 其中，fm为S中出现的所有函数符号的集合，t1, t2, tn为Hi-1的元素，i1，2, 则规定H称为G的H域（或说是相应的子句集S的H域）。Hi称为S的i水平常量集。不难看出，H域是直接依赖于G的，而且最多只有可数个元素。 例题2-4设子句集S = P(x), Q(y,f(z,b),R(a)，求H域解：H0 a, b为子句集中出现的常量H1 a, b, f(a,b), f(a,a), f(b,a), f(b,b)H2 a, b, f(a,b), f(a,a), f(b,a), f(b,b)， f(a,f(a,b), f(a,f(a,a), f(a, f(b,a), f(a, f(b,b), f(b,f(a,b), f(b,f(a,a), f(b, f(b,a), f(b, f(b,b), f(f(a,b),f(a,b), f(f(a,b),f(a,a), f(f(a,b), f(b,a), f(f(a,b), f(b,b), f(f(a,a),f(a,b), f(f(a,a),f(a,a), f(f(a,a), f(b,a), f(f(a,a), f(b,b), f(f(b,a),f(a,b), f(f(b,a),f(a,a), f(f(b,a), f(b,a), f(f(b,a), f(b,b), f(f(b,b),f(a,b), f(f(b,b),f(a,a), f(f(b,b), f(b,a), f(f(b,b), f(b,b)H = H1H2H3解毕注意：一个函数中含有多个变量时，每个变量都要做到全部的组合。原子集A：为研究子句集S中的不可满足性，需要讨论H域上S中各谓词的真值。这里原子集A为公式中出现的谓词套上H域的元素组成的集合。A = 所有形如 P(t1, t2, tn)的元素。这里，P(x1, xn)为出现于S中的任一谓词符号，而t1, t2, tn为S的H域中的任意元素。即把H域中的东西填到S的谓词里去。上例题的原子集为：A = P(a), Q(a,a), R(a), P(b), Q(b,a), Q(b,b), Q(b,a), R(b), P(f(a,b), Q(f(a,b), f(a,b), R(f(a,b), P(f(a,a), P(f(b,a), P(f(b,b),) 一旦原子集内真值确定好（规定好），则S在H上的真值可确定。不可数问题转化成为了可数问题。S中的谓词是有限的，H是可数的，因此，A也是可数的。论域D上公式G或子句集S的H域的建立，仅依赖于S中出现的几个函数符号，以及S中出现的D的几个常量符号，或D中的一个常量符号，这些都是可数的H域比一般论域D简单的原因。2.6.1.3 H解释解释I：谓词公式G在论域D上任何一组真值的指定称为一个解释。H解释：子句集S在H域上的解释称为H解释。I是H域下的一个指派。简单地说，原子集A中的各元素真假组合都是H的解释（或真或假只取一个）。或者说凡对A中各元素真假值的一个具体设定，都是S的一个H解释。由子句集S建立H域、原子集A，希望定义于一般论域D上使S为真的任一解释I，可由依于S的H域上的某个解释I*来实现。这样，便使任意论域D上S为真的问题，化成了仅有可数个元素的H域上S为真的问题了。从而子句集S在D上不可满足问题化成了H上的不可满足的问题。几个术语的定义：没有变量出现的原子、文字、子句和子句集，分别称为基原子、基文字、基子句和基子句集。基例：子句集S中某子句C中所有变元符号均以S的H域中的元素代入时，所得的基子句C称为C的一个基例。若一个解释I*使得某个基子句为假，则此解释I*为假。例：SP(x)Q(x), R(f(y)，求其一个H解释I*解：S的H域为：a, f(a), f(f(a), S的原子集为：P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), 凡对A中各元素真假值的一个具体设定都为S的一个H解释。如：I1*P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), I2*P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), I3*P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), I1*，I2*，I3*中出现的P(a)表示P(a)的取值为T，出现的P(a)表示P(a)的取值为F。显然在H域上，这样的定义I*下，S的真值就确定了。如：S| I1*T，S| I2*F，S| I3*F这是因为子句集SP(x)Q(x), R(f(y)的逻辑含义为：(x)(y)(P(x)Q(x)R(f(y)，论域H为a, f(a), f(f(a), 。关键：对于公式G的所有的解释，如果公式取值全为假，才可以判定G是不可满足的。因为所有解释代表了所有的情况，如果这些解释可以被穷举，我们就可以在有限的步数内判断公式G的不可满足性，本小节开始所提的问题便可解决 。我们所关心的是，对论域D上的任一个解释，若有S|I = T，如何求得一个相应的H解释，使得S|I* = T成立。可以证明，有如下三个定理：定理：定理1：设I是S的论域D上的解释，存在对应于I的H解释I*，使得若有S|I = T，必有 S|I* = T。定理2：子句集S是不可满足的，当且仅当S的一切H解释都为假。 定理3：子句集S是不可满足的，当且仅当对每一个解释I下，至少有S的某个子句的某个基例为假。以上三个定理保证了归结法的正确性。因为它们把S在一般论域D上的不可满足问题化成了可数集H上的不可满足问题。今后的讨论只需在S的H域上进行了，不必再涉及一般论域D。对于定理3来说，其结果经常被引用。因为S的逻辑含义是所包含的子句的合取，而且变量受全称量词的作用。那么在某个解释I（均指H解释）下为假，只需某个子句的某个基例为假，而S是不可满足的，要求在任一解释下均为假，从而定理3成立。 一般来说，D域是无穷不可列的，因此，子句集也是无穷不可列的。但子句集S确定后其H域是无穷可列的。不过在H上证明S的不可满足性仍然是不可能的。解决问题的方法：语义树。2.6.2 语义树与Herbrand定理对S的不可满足性，从几何上进行一些讨论是有益的。可以将子句集S的所有可能解释展示在一棵树上，进而观察每个分枝对应的S的逻辑真值是真是假。语义树的构成方法如下原子集A中所有元素逐层添加到一棵二叉树，并将元素的是与非分别标记在两侧的分枝上。下面是一个语义树的例子：例：对子句集SP(x)Q(x)，P(f(y)，Q(f(y)，画出相应的语义树。解：子句集S的H域为：Ha，f(a)，f(f(a)，原子集为AP(a)，Q(a)，P(f(a)，Q(f(a)，从A出发便可画出S的语义树，如下图所示：图2-2 无限语义树t2-2_swf.htm一般情况H是无限可数集，因此，S的语义树是无限树。 语义树的意义语义树可以理解为H域的图形解释。通过子句集S H域 原子集A 语义树。可以看出，我们讨论的对象从无限、不可数论域D转换成为可数的、有序的语义树。定义：完全语义树：S的语义树是完全的，如果对该语义树的所有叶结点N来说，I(N)包含了S的原子集AA1，A2，中的所有元素Ai或Ai，i=1 n 建立语义树的目的是把S中的每个解释都摊开。通过对S的完全语义树的观察，如上例的语义树图，这棵树的每个直到叶结点的分枝都对应于S的一个解释。特别对有限树来说，若N是叶结点，那么I(N)便是S的一个解释。讨论S的不可满足性，就可通过对语义树的每个分枝计算S的每一个解释的真值而实现。 有时并非需要无限地延伸某个分枝方能确定在相应的解释下S取假值。如果某个分枝延伸到结点N时，I(N)已使S的某一子句的某一基例为假，就无需再对N作延伸了。定义失败结点：当（由上）延伸到点N时，I(N)已表明了S的某子句的某个基例为假。但N以前尚不能判断这事实。就称N为失败结点。 封闭语义树：如果S的完全语义树的每个分枝上都有一个失败结点，就称它是一棵封闭语义树。图2-2所示的完全语义树便具有每个分枝上都有失败结点这样的性质，从而是一棵封闭的语义树。如果从图2-2剪去所有失败结点以下的分枝，便得相应的封闭语义树，见图2-3：图2-3 封闭语义树t2-3_swf.htm如I(N22)P(a)，Q(a)，这个S的部分解释已使S中的子句P(x)Q(x)的基例P(a)Q(a)为假了，而N11，N0不具有这个性质。若将I(N22)进一步扩充，仍然会使S为假，扩充的部分对使S为假已经不起作用了。从图上看无需对N22再作延伸了。Herbrand定理：定理1：子句集S是不可满足的，当且仅当对应于S的完全语义数是棵有限封闭树。 定理2：子句集S是不可满足的，当且仅当存在不可满足的S的有限基例集。 定理的意义在于将一阶逻辑证明问题转化成了有限的命题逻辑问题。由此定理保证，可以放心的用机器来实现自动推理了。（归结原理）注意：Herbrand定理给出了一阶逻辑的半可判定算法，即仅当被证明定理是成立时，使用该算法可以在有限步得证。而当被证定理并不成立时，使用该算法得不出任何结论。使用Herbrand定理，来证明定理或S是不可满足的，或是寻找有限的封闭树或是寻找有限的不可满足的基例集。一个具体实现证明的方法