Herbrand定理

,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,Herbrand定理,王珏 张文生,1,内容,Skolem范式,Herbrand域,语义树,Herbrand定理,Davis的工作,2,复习,定义(定理),如果G是公式F,1, F,2, F,n,的逻辑结论, 则公式,(F,1,F,2,F,n,)G,称为定理.,定理,给定公式F,1, F,2, F,n,和G, G是公式F,1, F,2, F,n,的逻辑结论, 当且仅当公式,F,1,F,2,F,n,G,不相容 (是永假式)。,3,化公式为Skolem范式的步骤,公式化为前束范式。,母式化为合取范式。,在不影响公式的不相容性的前提下, 使用,Skolem,函数，将前束中的存在量词消去。,4,Skolem,函数,消去存在量词;,令公式H是一个前束范式，并且母式M是合取范式,(Q,1,x,1,)(Q,n,x,n,)(M),对前缀从左到右遇到的第一个存在量词,Q,r,(1,r,n), 存在两种情况:,(1) 如果Q,r,的左边(前边)没有全称量词, 则M中的x,r,用常数a代替;,(2) 如果Q,r,的左边(前边)有全称量词x,s1,x,sk, 且1,s,1,s,k,r,则M中的x,r,用函数f(x,s1,x,sk,)代替;,从前缀中删除(,Q,r,x,r,);,5,Skolem,函数的意义,化公式为Skolem范式与原来公式在不相容意义下保持等价(=).,定理,: 令G是一个前束合取范式，,G=(Q,1,x,1,)(Q,n,x,n,)Mx,1,x,n,，,Q,r,为G中从左向右遇到的第一个存在量词。令,G,1,=(Q,1,x,1,)(Q,r-1,x,r-1,)(Q,r+1,x,r+1,)(Q,n,x,n,),Mx,1,x,r-1, f(x,1,x,r-1,),x,r+1,x,n,其中：f(x,1,x,r-1,)是x,r,的Skolem函数.,则有： G不相容,G,1,不相容,6,注意,Skolem范式和原式在不相容意义下保持等价, 而非等价(=)。,如果G不相容, 那么按照定理G=G,1,。,如果G是相容的，一般情况下，G不等价于G,1,，即：G,G,1,。,例子:,G =(,x)P(x),G,1,=P(a),在解释I下不相等:,D=1,2,a=1, P(1)=F, P(2)=T.,G在I下为真, G,1,在I下为假.,7,子句集,Skolem化以后, 将公式表示为子句集合.,(,x,)(,y,)(P(x),Q(y), (Q(x)S(f(y),P(x),Q(y), Q(x)S(f(y),定义(子句, clause):,一个包含若干文字的析取式称为子句。例如：,P, S,R,P(x),Q(y, z),R(y, y),说明：,一个子句中没有文字则称空子句(, nil,永假)；,一个子句中有n个文字则称n文字子句。,定义（子句集合）:,子句内部的关系是析取;,子句间的关系是合取;,所有子句受全程量词约束;,8,总结,定理,（公式不相容基本定理,）,设S是公式G的子句集,G不相容,S不相容,说明：,S不相容: 对任一个解释, S中至少有一个子句为假;,S相容: 存在一个解释, 使S中所有子句为真;,9,推论：,如果G=G,1,G,n, S,i,是G,i,的子句集, i=1,n. 令S=S,1,S,n,.,G不相容,S不相容,10,公式不相容基本定理的应用,定理证明思路,证明定理,G;,证明,G,不相容;,证明,G,的,Skolem,范式,G,1,不相容;,证明,G,1,的子句集不相容。,11,Skolem,范式,Herbrand,域,语义树,Herbrand,定理,Davis,的工作,12,一阶逻辑下验证定理是困难的原因:,个体变量论域D的任意性.,D中元素的任意性.,解释的个数的无限性.,我们试图找到：,一个比较简单的、特殊的论域，使得只要在这个论域上该公式是不可满足的，便能保证该公式在任一论域上也是不可满足的?,Herbrand域(简称H域)就具有这样的性质。,13,Herbrand域,令H,0,是子句集S中出现的常量的集合。若S中没有常量出现, 则H,0,由单个常量a组成(即H,0,=a)；,对于i=1,2,H,i,=H,i-1,所有形如f(t,1,.,t,n,)的项的集合,其中：f(t,1,.,t,n,)是出现于S中的任一函数符号t,1,.,t,n,H,i-1,。,规定,H,为S的,Herbrand,域（,Herbrand universe of S,简称H域,）。,14,基本概念,定义（基础，ground)：,没有变量的项，称为基础项(ground term).,f(a,b),没有变量的原子，称为基础原子(ground atom).,P(a,f(b),没有变量的文字，称为基础文字(ground literal).,P(a,f(b), P(a,f(b),没有变量的子句，称为基础子句(ground clause).,P(b,f(b), Q,(f(f(b),15,原子集,定义：,令S是一个子句集合，形如P(t,1,.,t,n,)的,基础原子,集合，称为S的原子集，或Herbrand基，记为A。,其中：,P(t,1,.,t,n,)是出现在S中的任一谓词符号, 而t,1,.,t,n,是S的,H域的任意元素,。,16,例子,S=P(z), P(x)Q(y),H,=a,A=P(a), Q(a),S=P(a), P(x)P(f(x),H,=a, f(a), f(f(a),.,A=P(a), P(f(a), P(f(f(a),， P(a),P(f(a)，,S=P(f(x), a, g(y), b),H,=a, b, f(a), g(a), f(b), g(b),A=P(a,a,a,a), P(a,a,a,b), P(a,a,b,b),.,17,基础实例,定义：,当S中的某子句C中,所有变量符号,均以S,的H域的元素代入,时，所得的基子句C称作C的一个基础实例(基例， a ground instance of a clause C),。,例 S=P(x), Q(f(y)R(y), Z(f(y),H=a,f(a),f(f(a),.,P(a), P(f(a)都称作子句C=P(x)的基例。,同样, Q(f(a)R(a), Q(f(f(a)R(f(a)都是Q(f(y)R(y)的基例。,对于任一bD,子句P(b), Q(f(b)R(b)都叫基子句。,但是，Q(a)R(a)不是Q(f(y)R(y)的基础实例。,18,注意,原子集和基础实例不同：,原子集考虑单个,原子,，基础实例考虑,子句,。,Q(f(a)R(a)是基例，但不属于S的原子集。,原子集是将某个谓词中的,项,改为H域中的元素，而基例是改,变量,。,H=a,f(a),f(f(a),.,Q(a)不是Q(f(y)的基例, 但是属于S的原子集。,Q(f(a)既是Q(f(y)的基例, 又属于S的原子集。,一个,基础实例,是由原子集中的原子或原子的非,析取,而成。,A=P(a), Q(a),R(a), Z(a), P(f(a),Q(f(a),.,基础实例:,Q(f(a),R(a),19,H解释,起因,由子句集,S,建立,H,域，进而容易得到原子集,A；,一般论域,D,上对,S,的解释,I,H,域上的解释,I*,;,S在D,上为真,S在H,上为真;,S,在,D,上不可满足,S,在H上不可满足。,20,H解释的表示,令A=A,1,A,n,是S的原子集, 一个H解释可被表示为:,I=m,1,m,n,其中：m,j,或者是A,j,，或者是A,j,。,如果m,j,是A,j, 则A,j,为真, 否则, A,j,为假。,21,H解释的性质,引理,如果在论域D上的一个解释I满足S，则任一个对应于I的H解释I*，也满足S。,定理,子句集S是不可满足的，,当且仅当,S的所有的H解释使S为假。,22,结论：,如果S为不满足的，则存在一个特殊域，当S被证明在这个域上的所有解释为F。,即证明了对所有域上的所有解释为F，也就证明了S为不相容的。,23,几个性质,性质1:,一个子句,C,的基础实例,C被,解释,I,满足, iff,存在一个,C,的基础文字,L,在,I下为真,即,C,I,。,C: P(x), Q(f(x),H: a, f(a), f(f(a),C:,P(a), Q(f(a),I,1,: ,P(a), Q(a), P(f(a), Q(f(a), ,性质2:,一个子句,C,在解释,I,下为真，,iff,这个子句,C,的每个基础实例被,I,所满足。,I,2,: ,P(a), Q(a), P(f(a), Q(f(a), ,24,性质3:,一个子句,C,在解释,I,下为假，,iff,至少存在一个,C,的基础实例,C,，使得,C,不被,I,所满足。,C: P(x), Q(f(x),H: a, f(a), f(f(a),C:P(a), Q(f(a),I,3,: ,P(a), Q(a), P(f(a),Q(f(a), ,性质4:,子句集,S,是不可满足的,iff,对每个解释,I,下，至少有,S,的某个子句的某个基例不被,I,所满足。,25,Skolem范式,Herbrand域,语义树,Herbrand定理,Davis的工作,26,语义树,(Semantic tree),例1,G = P,Q,R,S = P,Q, R,A = P,Q, R,P,P,Q,Q,Q,Q,R,R,R,R,R,R,R,R,27,例2,S=P(x),Q(x), P(f(y), Q(f(y),H=a, f(a), f(f(a), .,A=P,(,a), Q(a), P(f(a), Q(f(a), .,P(a),P(a),Q(a),Q(a),Q(a),Q(a),P(f(a),P(f(a),P(f(a),P(f(a),P(f(a),P(f(a),. ,28,注意,颠倒原子的顺序是可以的. 例如Q(a)为第一个顶点.,如果原子集,是无限的，则对应的语义树必定是无限的.,从任一个叶节点向根节点看, 代表S的一个解释.,从任一个中间节点向根节点看, 代表S的一个部分解释.,29,一些概念,定义(complementary pair, 互补对),如果,A,是一个原子, 那么两个文字,A,和,A,成为互补对, 并且 ,A, A, 称为互补对。,包含互补对的子句是永真的.,P, Q Q,30,定义,(semantic tree, 语义树),给定一个子句集,S,，令A是一个S的原子集合，一个对S来说的语义树是一个向下的树结构,T, 在它的每一条联线上均附加了一个有限的在A中的原子或原子非的集合:,对于每一个节点,N, 仅有有限个直接联线,L,1,L,n,，令,Q,i,是附加在,L,i,（ i=1,n）,的所有文字的合取，,则,Q,1,Q,n,是一个永真的命题（基础）.,对于每一个节点,N, 令,I(N),是从根节点到,N,节点的一个分支上的所有附加在个联线上文字集合的并集（包含N），则,I(N),不包含任何互补对。,注意,：,I(N),不是一个解释，它仅是一个解释的一部分,。,31,完备语义树（complete semantic tree）,定义:,假设 A=A,1, A,2, , A,k, 是子句集S的原子集合，一个对S来说的语义树是完备的，iff 对这个语义树的每一个端节点,N,，,I(N),包括A,i,或 A,i, 对i=1,2,都成立.,32,例1,G = P,Q,R,S = P,Q, R,A = P,Q, R,P,P,Q,Q,Q,Q,R,R,R,R,R,R,R,R,33,P,P,Q,Q,Q,Q,R,R,R,R,P,P,Q,Q,Q,Q,R,R,R,R,反例,34,完备语义树的性质,一个完备的语义树是对一个公式的全部解释 (全部),当原子集 A 无限时, 任何完备语义树S 兼时无限的 (无限),如果S是不可满足的, 那么从某一个节点,N,以后我们可以停止扩展. (终止),35,封闭语义树(Closed semantic tree),定义(failure node, 失败节点, 假节点),如果,I(N),使,S,中的某个字句的基础实例为假，但是，,I(N),不能使,S,中的任何子句为假，,N,为,N,的父亲节点，则称,N,为假节点。,36,例,S=P, Q,R, P,Q, P,R,P,P,Q,Q,Q,Q,R,R,R,R,R,R,R,R,37,定义(Closed semantic tree, 封闭语义树),一个语义树T是封闭的，iff T的每一个分支终止在假节点。,S=P, Q,R, P,Q, P,R,P,P,Q,Q,R,R,38,例,S=P(x), P(x),Q(f(x), Q(f(a),A=P(a), Q(a), P(f(a), Q(f(a),P(a),Q(f(a),P(a),Q(f(a),39,推理节点,定义(inference node, 推理节点),如果在一个封闭的语义树中，节点,N,的直接子孙均为假节点，则这个节点N为推理节点.,S=P(x), P(x),Q(f(x), Q(f(a),A=P(a), Q(a), P(f(a), Q(f(a),P(a),Q(f(a),P(a),Q(f(a),40,证明一个定理就是寻找一棵封闭语义树.,S不可满足, S在所有解释下为假 S在所有H解释下为假;,完备语义树包含所有H解释，并且每一枝是一个H解释;,S在I下为假, 则使某个基础实例为假;,对于假节点, 语义树不用再扩展;,所有枝上都有假节点, 则为封闭语义树;,41,Skolem范式,Herbrand域,语义树,Herbrand定理,Davis的工作,42,Herbrand定理,定理(Version 1),子句集,S,是不可满足的，,当且仅当,对应于,S,的任一棵完备语义树, 都存在一棵有限的封闭语义树。,43,证明,（,=,）,设子句集,S,不可满足.,要证:对应于,S,的任一棵完备语义树, 都存在一棵有限的封闭语义树。,设T是S的完备语义树.,任选T的一个分支B, I(B)是B上所有连线上的文字的集合的并， I(B)是S的一个解释.,S不可满足, 则I(B)一定使S中的一个子句C为假;,I(B)一定使C的某个基础实例C为假(,性质3,);,因为C的每个原子一定都在原子集A中，并且 C的文字数目是有限的, 所以在B上一定存在一个假节点.,因为B的任意性, T的每个分支都有假节点.,因此， T是封闭的.,44,T是有限的.,T是有限的封闭语义树.,（,） 设,子句集,S,是不可满足的;,要证: 存在一个有限不可满足的S的基础实例集合S.,根据Version 1, 有一棵有限的封闭语义树;,每一枝都终止在假节点上， 每一枝都使,S,的某个子句的某些基例为假， 构成S.,S不可满足.,有限的封闭语义树 ,节点,有限 ,假节点有限；,因此， S有限.,47,（,=,）,设存在一个有限不可满足的S的基础实例集合S。,S的任一个解释I都是一个对所有基础实例的解释;它包含一个对S的解释I.,因为S不可满足, 所以I使S为假;,I,I, 所以I使S为假; (I使某个子句的某个基础实例为假),由于解释I的任意性, 因此，S不可满足.,48,说明,：,S不相容就是对S的每一个解释均使S为假，事实上，就是存在一个有限封闭的语义树，进一步就是存在一个基础实例集。,如何找到一个封闭的语义树或有限的字句的基础实例集元不是件容易的事。,Herbrand定理仅仅是一个存在型定理,。,49,例2. S= P(x),Q(f(x),x) ,P(g(x), Q(y,z) ,H=a, f(a), g(a), g(f(a), f(g(a), ,A= ,S,1,=,P(g(a), Q(f(g(a), g(a) , P(g(a), Q(f(g(a), g(a),S不相容,50,例2. S=P(x), P(f(x),H=a, f(a), f(f(a), ,A= P(a), P(f(a), P(f(f(a),S,1,=P(f(a), P(f(a),S不相容,51,寻找封闭语义树的步骤：,求H域,求H基A,构造完备的语义树,求假节点,形成封闭的语义树,52,Gilmore的方法(1960),子句集S是有限的;,基础实例的数目是可数的;,枚举;,53,Skolem,范式,Herbrand,域,语义树,Herbrand,定理,Davis,的工作,54,Davis-Putnam的工作,Gilmore的方法是,指数复杂性,的;,Davis-Putnam: 提高效率(,启发式方法,);,预备知识,：,空子句永假；,（注：空子句是指集合中有一个空子句）；,空集合永真；,（空集合是指没有元素的集合）；,重言式子句：包含互补对的子句。,四条规则,:,注意：下面规则的应用不改变子句集的不相容性。,55,规则一：重言式规则(tautology rule),S中的重言式子句，不会为S的不可满足提供任何信息，应该删除。,例如：S=PP，Q，RPS的逻辑含义是（,PP,）Q(RP)= Q(RP)，从而删去重言式,PP,，不影响S的真值。,S=Q，RP,56,规则二：,单文字规则(one-literal rule),如果在S中存在只有一个文字的基础子句L, 消去在S中,带有这个文字L的,所有子句,得到S, 如果S为空, 则S是相容的;,否则, 从S中,删去,L, 得到S，则 S不可满足,当且仅当,S不可满足.,单文字: 在S中存在只有一个文字的基础子句L.,例子: S=,L,，,LP,，,LQ,，S,R,S = LQ,，S,R S= Q,，S,R,S不可满足, 则在所有解释下S都为假;,L=F;,L=T;,L=F.,57,规则三：,纯文字规则(pure-literal rule),L是S的纯文字. 从,S,中,删除含,L,的子句,得,S,，如果,S,为空集，那么,S,是可满足的;,否则, S不可满足,当且仅当,S不可满足.,纯文字:,如果文字L出现于S中，而L不出现于S中，L称为S的纯文字.,例子: S=,A,B,A,B, B, B,S= B, B;,S不可满足, 在A为真的情况下不可满足;,A=1,AB=1, AB=1;,S不可满足, 当然S不可满足;,58,规则四,分裂规则(splitting rule),S=,(LA,1,). (LA,m,) ,(LB,1,). (LB,n,)R,其中：A,i,B,i, R中不含L和L（,自由,）。令S =A,1,.A,m,R， S=B,1,.B,n,R则S不可满足,当且仅当,S和S同时是不可满足，,即：S,S同时是不可满足。,59,例1. S=P,QR, PQ, P, R,U,对U使用纯文字: P,QR, PQ,P, R,对P使用单文字: ,QR,Q, R,对Q使用单文字: ,R,R,对,R,使用单文字: ,S不可满足;,注意：如果 L是单文字基础子句，当L从这个子句集合中被删去后，则这个子句为空子句。,60,例2. S=P,Q,Q, PQR,对Q使用单文字: ,P, PR,对P使用单文字: ,R,对R使用纯文字: ,S可满足;,61,例3. S=,P,Q,P,Q,QR, QR,用规则4：S,1,= Q, QR， QR,S,2,= Q, QR， QR,在S,1,中，对Q使用单文字: R,在S,2,中，对Q使用单文字: R,则得到： S,1, S,2,= ,R,对,R,使用纯文字: ,S可满足;,62,例4.,S=,P,Q,P,Q, RQ, RQ,用规则3： Q,R,， Q,R,用规则3： ,S可满足;,63,注意：,这些规则对于命题逻辑是十分有效的，但是，对于一阶为词逻辑则需要寻找基础实例集。,Davis的工作在理论上是十分重要的，它对于后来的归结原理的证明方法齐了重要的作用。,64,练习,写出下式的H域和原子集.,S=P(f(x,a),S=P(x)Q(y), R(f(y),前提,：每个储蓄钱的人都获得利息。,结论,：如果没有利息，那么就没有人去储蓄钱。令：S（x，y）表示x储蓄y M（x） 表示x是钱I（x） 表示x是利息E（x，y） 表示x获得y,用逻辑公式表示前提和结论并化为子句形式;,下述子句集是可满足的还是不可满足的(给出过程)?,S=PQ, PQ, PQ, PQ,65,