,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,单击此处编辑母版标题样式,第,5,章 谓词逻辑的等值和推理演算,谓词逻辑研究的对象是重要的逻辑规律，普遍有效式是最重要的逻辑规律，,而等值式、推理式都是普遍有效的谓词公式，,因此等值和推理演算就成了谓词逻辑的基本内容,这章的讨论，主要是以,语义的观点,进行的非形式的描述，而严格的形式化的讨论见第,6,章所建立的公理系统,第5章 谓词逻辑的等值和推理演算谓词逻辑研究的对象是重要的,1,5,1,否定型等值式,等值：,若给定了两个谓词公式,A,，,B,，说,A,和,B,是等值的，如果在公式,A,，,B,的任一解释(,注意在谓词逻辑中，解释的范围还包含论域以外的其他要素，见,P65,),下，,A,和,B,都有相同的真值,其他说法：,A,，,B,等值当且仅当,AB,是普遍有效的公式(注意这里不再说重言式了)记作,A,B,或,A,B。,51 否定型等值式等值：若给定了两个谓词公式A，B，说A,2,5,1,1,由命题公式移植来的等值式,若将命题公式的等值式，直接以谓词公式代入命题变项便可得谓词等值式由,p,p,pq=pq,(pq)r=(pr)(qr),可得(以下每两个为一对：无量词、有量词),P(x),P(x),(,x)P(x),(,x)P(x),P(x)Q(x),P(x)Q(x),(,x)P(x)(,x)Q(x),(,x)P(x)(,x)Q(x),(P(x)Q(x)R(x)=(P(x)R(x)(Q(x)R(x),(,x)P(x)Q(y)(,z)R(z),=(,x)P(x)(,z)R(z)(Q(y)(,z)R(z),511 由命题公式移植来的等值式若将命题公式的等值式，,3,5,1,2,否定型等值式（摩根律的推广）,(,x)P(x)=(,x)P(x),(,x)P(x)=(,x)P(x),形式上看这对公式，是说否定词”,”,可越过量词深入到量词的辖域内，但要把所越过的量词,转换为,，,转换为,.,512 否定型等值式（摩根律的推广） (x)P,4,(1),从语义上说明,(2),例：在,l,，,2,域上分析,(,x)P(x)=,(P(1),P(2)=P(1)vP(2),=(,x),P(x),(,x)P(x)=,(P(1)vP(2)=P(1),P(2),=(,x),P(x),(1)从语义上说明(2)例：在l，2域上分析(x,5,(3),语义上的证明,证明方法：依等值式定义，,A=B,如果在任一解释,I,下,A,真,B,就真，而且,B,真,A,就真,若证明,(,x)P(x)=(,x)P(x),1. 设某一解释,I,下若,(,x)P(x)=T,从而,(,x)P(x)=F,，即有一个,x,o,D,使,P(X,o,)=F,于是,P(x,o,)=T,故在,I,下,(,x)P(x)=T,2. 反过来，设某一解释,I,下若,(,x) P(x)=T,即有一个,x,o,D,使,P(X,o,)=T,从而,P(X,o,)=F,于是,(,x) P(x)=F,即,(,x)P(x)=T,(3)语义上的证明证明方法：依等值式定义，A=B如果在任一解,6,(4),举例,例,1 “,并非所有的动物都是猫”的表示,设,A(x),：,x,是动物,B(x),：,x,是描,原语句可表示成,(,x)(A(x),B(x),依否定型公式得,(4)举例例1 “并非所有的动物都是猫”的表示,7,例,2 “,天下乌鸦,般黑”的表示,设,F(x),：,x,是乌鸦,G(x,，,y),：,x,与,y,是一般黑,原语句可表示成,(,x)(y)(F(x)F(y),G(x,y),不难知道与之等值的公式是,(,x)(y)(F(x)F(y),G(x,y),即不存在,x,y,是乌鸦但不一般黑这两句话含义是相同的经计算有,例2 “天下乌鸦般黑”的表示,8,全称量词消去课件,9,5,2,量词分配等值式,一、含单独的命题变项，与,x,无关,5,2,1,量词对,、,的分配律,这是一组量词对,、,的分配律，其中,q,是命题变项，与个体变元,x,无关，这是很重要的条件,我们仅对第一个等式给出证明，其余三个同样可证,52 量词分配等值式一、含单独的命题变项，与x无关,10,设在一解释,I,下，,(,x)(P(x),q)=T,，从而对任一,x,D,，有,P(x),q=T,若,q,T,，则,(,x)P(x),q=T,若,q,F,，从而对任一,x,D,，有,P(x) =T,，即有,(,x)P(x)=T,，故仍有，,(,x)P(x),q=T,反过来，设在一解释,I,下，,(,x)P(x),q=T,，,若,q=T,，则,(,x)(P(x),q)=T,若,q=F,，必有,(,x)P(x)=T,，从而对任一,x,D,有,P(x)=T,，于是对任一,x,D,有,P(x),q=T,故,(,x)(P(x),q)=T,设在一解释I下，(x)(P(x)q)=T，从而对任一x,11,5,2,2,量词对,的分配律,这是一组量词对,的分配律，其中,p,，,q,是命题变项，与个体变元,x,无关，这是很重要的条件,5.2节介绍的等值公式中仅有这里的第一、二个公式有量词的改变！,522 量词对的分配律,12,先证明其中的第一个等式,依,5,2,1,的等值式,依,5,l,2,的等值式,先证明其中的第一个等式,13,再证明其中的第三个等式,依,5,2,l,的等值式,其余两个等值式同样可证,再证明其中的第三个等式,14,二、辖域中无单独的命题变项,5,2,3,量词,对,、量词,对,V,的分配律,这是当,P(x),，,Q(x),都含有个体变元,x,时，量词,对,，量词,对,V,所遵从的分配律然而,对,V,，,对,的分配律一般并不成立证明中使用了5.2.1中的解释方法。,(,x)P(x)v(x)Q(x)=(x)(P(x)vQ(x),(,x)(P(x)Q(x)=(x)P(x)(x)Q(x),二、辖域中无单独的命题变项523 量词对 、量词,15,一些例子,一些例子,16,5,2,4,变元易名后的分配律(在求前束范式时有很大作用),这两个等值式，说明了通过变元的易名，仍可实现,对,V,，,对,的分配律,证明是容易的首先有变元易名等值式,(,x)P(x)= (,y,)P(y),(,x)P(x)= (,y,)P(y),于是,(,x)P(x)v(x)Q(x)=,(,x)P(x)v(y)Q(y),524 变元易名后的分配律(在求前束范式时有很大作用,17,对,x,而言,(,y)Q(y),相当于命题变项，与,x,无关，可推得,(,x)P(x)v(,y)Q(y)=(,x)(P(x)v(,y)Q(y),对,y,而言，,P(x),相当于命题变项与,y,无关，又可推得,(,x)(P(x)v(,y)Q(y)=(,x)(,y)(P(x)vQ(y),同理,(,x)(,y)(P(x)Q(y)=(,x)P(x)(,x)Q(x),然而,(,x)(,y)(P(x)vQ(y),与,(,x)(P(x)vQ(x),是不等值的,(,x)(,y)(P(x)Q(y),与,(,x)(P(x)Q(x),也是不等值的,对x而言(y)Q(y)相当于命题变项，与x无关，可推得,18,5,3,范 式,在命题逻辑里每一公式都有与之等值的范式，范式是一种统一的表达形式,对谓词逻辑的公式来说也有范式，其中,前束范式与原公式是等值的,，而其他范式与原公式只有较弱的关系。,53 范 式在命题逻辑里每一公式都有与之等值的范,19,5,3,1,前束范式,定义,5,3,1,说公式,A,是一个前束范式，如果,A,中的一切量词都位于该公式的最左边,(,不含否定词,),且这些量词的辖域都延伸到公式的末端，前束范式,A,的一般形式为,(Q,1,x,1,)(Q,n,x,n,)M(x,l,，,，,x,n,),其中,Q,i,为量词,或,(i,l,，,，,n),，,M,称作公式,A,的,母式,(,基式,),，,M,中,不再有量词,定理,5,3,1,谓词逻辑的任一公式都可化为与之,等值的,前束范式但其前束范式,并不唯一,531 前束范式定义531 说公式A是一个前束范,20,全称量词消去课件,21,经过这几步，便可求得任一公式的前束范式由于每一步变换都保持着等值性，所以，所得到的前束形与原公式是等值的,这里的,S(a,，,b,，,x,，,y,，,z),便是原公式的母式其中,a,b,为自由个体变项,。,由于前束中量词的次序排列，以及对母式都没有明确的限制，自然前束范式不是唯一的，如例,1,的前束范式也可以是,(,x)(z)(y)(S(a,b,x,y,z)P),其中,P,可以是任一不含量词的普遍有效的公式。,经过这几步，便可求得任一公式的前束范式由于每一步变换都保持,22,532 Skolem标准形,前束范式对前束量词没有次序要求，也没有其他要求如果对前束范式进而要求所有存在量词都在全称量词之左得到存在前束范式(略)，或是,只保留全称量词而消去存在量词,得到,Skolem,标准形。不难想像，仍保持与原公式的等值性就不可能了，只能保持在某种意义下的等值关系,532 Skolem标准形前束范式对前束量词没有次序要,23,(1),前束范式(略),一个公式的,前束范式为,(,x,1,)(,x,i,),(,x,i+1,)(,x,n,)M(x,1,，,，,x,n,),即存在量词都在全称量词的左边，且可保持,至少,有一个,存在量词,(i1),，其中,M(x,1,，,，,x,n,),中,不再含有量词也无自由个体变项,定理,5.3.2,谓词逻辑的任一公式,A,，都可化成相应的,前束范式，并且,A,是普遍有效的当且仅当其,前束范式是普遍有效的。,这定理是说对普遍有效的公式，它与其,前束范式是等值的，而一般的公式与其,前束范式并不是等值的,自然仅当,A,是普遍有效的，方使用,前束范式,(1) 前束范式(略)一个公式的前束范式为 (,24,例,2,求,(,x)(,y)(,u)P(x,，,y,，,u),的,前束范式,(P,中无量词,),将一公式化成,前束形，首先要求出前束形，再做,前束，这个例子已是前束形了，便可直接求,前束形,例2 求( x)( y)( u)P(x，y，u)的,25,首先将全称量词,(,y),改写成存在量词,(,y),，其次是引入谓词,S,和一个变元,z,，得,S(x,，,z),，建立公式,(,x)(,y)(,u)(P(x,，,y,，,u)S(x,，,y)V(,z)S(x,，,z),其中,S(x,，,y),的变元，是,(,y),的变元,y,和,(,y),左边存在量词,(,x),的变元,x,附加的,(,z)S(x,，,z),中的变元,z,是新引入的未在原公式中出现过的个体，,S,也是不曾在,M,中出现过的谓词,进而将,(,z),左移,(,等值演算,),，便得,前束范式,(,x)(,y)(,u)(,z)(P(x,，,y,，,u)S(x,，,y)VS(x,，,z),当原公式中，有多个全称量词在存在量词的左边，可按这办法将全称量词逐一地右移,前束范式仅在普遍有效的意义下与原公式等值,前束形对谓词逻辑完备性的证明是重要的,首先将全称量词( y)改写成存在量词( y)，其次是引入,26,改写前,=,改写后：简单,改写后,=,改写前：反证,若,A=(,x)(,y)(,u)P(x,，,y,，,u),不是普遍有效，则存在解释,I,使,A,为,F,于是,(,x)(,y)(,u)P(x,，,y,，,u),为,F.,因此在解释,I,下，改写后,B= (,x)(,z)S(x,，,z),可为,F,因为,S,是谓词变元。,改写前=改写后：简单,27,(2) Skolem,标准形,另一种,Skolem,标准形是仅保留全称量词的前束形,定理,5.3,.,3,谓词逻辑的任一公式,A,，都可化成相应的,Skolem,标准形,(,只保留全称量词的前束形,),，,并且,A,是不可满足的当且仅当其,Skolem,标准形是不可满足的,这定理是说对不可满足的公式，它与其,Skolem,标准形是等值的，而一般的公式与其,Skolem,标准形并不是等值的自然仅当,A,是不可满足的方使用,Skolem,标准形,.,(2) Skolem标准形另一种Skolem标准形是仅保留全,28,例,3,求公式,(,x,)(,y)(,z)(,u)(,v)(,w)P(x,y,z,u,v,w),的,Skolem,标准形,将一公式化成,Skolem,标准形，首先也要求出前束形这个例子已是前束形了，便可直接求,Skolem,标准形了,首先将最左边的,(,x),消去，而将谓词,P,中出现的所有变元,x,均以论域中的,某个常项,a,(a,未在,P,中出现过,且不知道,a,具体是哪个常量,）代入。,例3 求公式,29,进而消去从左边数第二个存在量词,(,u),，因,(,u),的左边有全称量词,(,y)(,z),，需将谓词,P,中出现的所有变元,u,均以,y,，,z,的,某个二元函数,f(y,，,z),(f,未在,P,中出现过，,且不知道,f,具体是哪个函数,),代,入,最后按同样的方法消去存在量词,(,w),，因,(,w),的左边有全称量词,(,y)(,z),和,(,v),，需将谓词,P,中出现的所有变元,w,均以,y,，,z,，,v,的某个三元函数,g(y,，,z,，,v)(g,未在,P,中出现过也不同于,f),代,入,这样便得消去全部存在量词的,Skolem,标准形,(,y)(,z)(,v)P(a,y,z,f(y,z),v,g(y,z,v),进而消去从左边数第二个存在量词(u)，因(u)的左边有全,30,54 基本的推理公式,命题逻辑中有关推理形式、重言蕴涵以及基本的推理公式的讨论和所用的术语，都可引入到谓词逻辑中并可把命题逻辑的推理作为谓词逻辑推理的一个部分来看待,这里所介绍的是谓词逻辑所特有的，在命题逻辑里不能讨论的推理形式和基本的推理公式。,54 基本的推理公式命题逻辑中有关推理形式、重言蕴涵以及,31,5,4 .1,推理形式举例,例,1,所有的整数都是有理数，所有的有理数都是实数，所以所有的整数都是实数,引入谓词将这三句话形式化，可得如下推理形式,:,(,x)(P(x)Q(x),(,x,)(Q(x)R(x),(,x)(P(x)R(x),54 .1 推理形式举例例1 所有的整数都是有理数，,32,例,2,所有的人都是要死的，孔子是人，所以孔子是要死的，引入谓词将这三句话形式化，可得如下推理形式：,(,x)(A(x)B(x),A(,孔子,)B(,孔子,),例2 所有的人都是要死的，孔子是人，所以孔子是要死的，引入,33,例,3,有一个又高又胖的人，必有一个高个子而且有,个胖子。,引入谓词将这两句话形式化，可得如下推理形式：,(,x)(C(x),D(x)(,x)C(x),(,x)D(x),例3 有一个又高又胖的人，必有一个高个子而且有个胖子。,34,例,4,若某一个体,a,具有性质,E,，那么所有的个体,x,都具有性质,E,这两句话形式化，可得如下推理形式：,E(a)(,x)E(x),不难看出，由例,1,，,2,，,3,所建立的推理形式是,正确的,，而例,4,的推理形式是,不正确的,例4 若某一个体a具有性质E，那么所有的个体x都具有性质E,35,5.4.2,基本的量词推理公式,(,x)P(x)V(,x)Q(x)=(,x)(P(x)VQ(x),量词分配律,p73,(,x)(P(x),Q(x)=(,x)P(x),(,x)Q(x),注意,(1)的逆否,例3,(,x)(P(x)Q(x)=(,x)P(x)(,x)Q(x),5.2.2,的推广,(,x)(P(x)Q(x)=(,x)P(x)(,x)Q(x),5.2.2,的推广,(5) (,x)(P(x),Q(x) )=(,x)P(x),(,x)Q(x),(3),的推广,(6) (,x)(P(x),Q(x)=(,x)P(x),(,x)Q(x),(4),的推广,5.4.2 基本的量词推理公式(x)P(x)V(x)Q,36,(7) (,x)(P(x)Q(x),(,x)(Q(x)R(x)=,(,x)(P(x)R(x),例1,(8) (,x)(P(x)Q(x),P(a)=Q(a),例2,(,x)(,y)P(x,y)=(,x)(,y)P(x,y),易理解,(,x)(,y)P(x,y)=(,y)(,x)P(x,y),易理解，注意右边,x,是,y,的函数,这些推理公式或称推理定理的逆一般是不成立的，所以正确地理解这些定理的前提与结论的不同是重要的。,(7) (x)(P(x)Q(x) (x)(Q(x,37,5.5,推理演算,命题逻辑中引入推理规则的推理演算，可推广到谓词逻辑，有关的推理规则都可,直接移入,到谓词逻辑，除此之外还需介绍,4,条有关量词的消去和引入规则,(,代入规则需补充说明：保持合式公式和普遍有效性不被破坏，见,p58),5.5 推理演算命题逻辑中引入推理规则的推理演算，可推广到,38,5,5,1,推理规则,(1),全称量词消去规则,(,x)P(x)=P(y),注：,1其中,y,是论域中任意一个体,2,需限制,y,不在,P(x),中约束出现(右侧量不在左侧约束出现),如,(,x)P(x),(,x)(,y)(xP(y),因,P(y),会有问题,551 推理规则(1)全称量词消去规则(x)P(x,39,(2),全称量词引入规则,P(y) =(,x)P(x),注：,1任一个体,y(,自由变项,),都具有性质,P,2仍需限制,x,不在,P(y),中约束出现,(,右侧量不在左侧约束出现),如,P(y),(,x)(xy),时，,P(x),会有问题,(2)全称量词引入规则P(y) =(x)P(x),40,(3),存在量词消去规则,(,x)P(x)=P(c),注,1.,c,是论域中使,P,为真的某个个体常项,2. 需限制,(,x)P(x),中没有自由个体出现,. 还需限制,P(x),中不含有,c,(右侧量不在左侧出现),如在实数域上,(,x)P(x)=(,x)(cP(c),的正确性,(3)存在量词消去规则(x)P(x)=P(c),41,(4),存在量词引入规则,P(c)=(,x)P(x),注：,1.,c,是论域中使,P,为真的一个特定个体常项,2. 需限制,x,不出现在,P(c),中,(右侧量不在左侧出现),如实数域上，,P(c),(,x)(xc),时，,P(x),会出问题,(4)存在量词引入规则P(c)=(x)P(x),42,这,4,条推理规则是基本的，对,多个量词下的量词消去与引入规则,的使用也已谈到再明确说明一下,(,x)(,y)P(x,，,y)=(,y)P(x,，,y),的右端，不允许写成,(,y)P(y,，,y),，,(,x)P(x,，,c)=(,y)(,x)P(x,，,y),的右端不允许写成,(,x)(,x)P(x,，,x),。,这4条推理规则是基本的，对多个量词下的量词消去与引入规则的使,43,(,x)(,y)P(x,，,y)=(,y)P(x,，,y)=P(x,，,a),但不允许再推演出,(,x)P(x,，,a),和,(,y)(,x)P(x,，,y),原因是,(,x)(,y)P(x,，,y),成立时，所找到的,y,是依赖于,x,的，从而,P(x,，,y),的成立是有条件的，不是对所有的,x,对同一个,a,都有,P(x,，,a),成立，于是不能再推演出,(,y)(,x)P(x,y),(x)(y)P(x，y)=(y)P(x，y)=P(,44,5,5,2,使用推理规则的推理演算举例,和命题逻辑相比，在谓词逻辑里使用推理规则进行推理演算同样是方便的，然而在谓词逻辑里，,真值表法不能使用,，又,不存在判明,AB,是普遍有效的一般方法,，从而,使用推理规则的推理方法已是谓词逻辑的基本推理演算方法,推理演算过程,首先,是将以自然语句表示的推理问题引入谓词形式化，,若,不能直接使用基本的推理公式便消去量词，在无量词下使用规则和公式推理，最后再引入量词以求得结论,552 使用推理规则的推理演算举例和命题逻辑相比，在谓,45,例,1,前提,(,x)(P(x)Q(x),，,(,x)(Q(x)R(x),结论,(,x)(P(x)R(x),证明,(1)(,x)(P(x)Q(x),前提,(2)P(x)Q(x),全称量词消去,(3)(,x)(Q(x)R(x),前提,(4)Q(x)R(x),全称量词消去,(5)P(x)R(x) (2),，,(4),三段论,(6)(,x)(P(x)R(x),全称量词引入,例1 前提 (x)(P(x)Q(x)，(x)(Q,46,例,2,所有的人都是要死的，苏格拉底是人，所以苏格拉底是要死的,首先引入谓词形式化，令,P(x),表,x,是人，,Q(x),表,x,是要死的，于是问题可描述为,(,x)(P(x)Q(x)P(,苏格拉底,)Q(,苏格拉底,),证明,(1)(,x)(P(x)Q(x),前提,(2)P(,苏格拉底,)Q(,苏格拉底,),全称量词消去,(3)P(,苏格拉底,),前提,(4)Q(,苏格拉底,),(2)(3),分离规则,例2 所有的人都是要死的，苏格拉底是人，所以苏格拉底是要死,47,例,3,前提,(,x)P(x)(,x)(P(x)VQ(x)R(x),，,(,x)P(x),结论,(,x)(,y)(R(x)R(y),证明,(1)(,x)P(x)(,x)(P(x)VQ(x)R(x),前提,(2)(,x)P(x),前提,(3)(,x)(P(x)VQ(x)R(x) (1),，,(2),分离,(4)P(c),(2),存在量词消去,(5)P(c)VQ(c)R(c) (3),全称量词消去,(6)P(c)VQ(c) (4),(7)R(c) (5),，,(6),分离,(8)(,x)R(x),(7),存在量词引入,(9)(,y)R(y) (7),存在量词引入,(10)(,x)R(x)(,y)R(y) (8),，,(9),(11)(,x)(,y)(R(x)R(y) (10),置换,例3 前提(x)P(x)(x)(P(x)VQ(x),48,例,4(,不正确,) 分析下述推理的正确性,(1)(,x)(,y)(xy),前提,(2)(,y)(zy),全称量词消去,y,与,z,有关,(3)zb,存在量词消去,b,依赖,z,(4)(,z)(zb),全称量词引入,b,不依赖,z,(5)bb,全称量词消去,(6)(,x)(xx),全称量词引入,推理,(1),到,(2),，应明确指出,y,是依赖于,x,的，即,(2),中,y,和,z,有关,(2),到,(3),，其中的,b,是依赖于,z,的从而,(3),到,(4),是不成立的又由于,b,是常项，,(5),到,(6),也是不允许的，因个体常项不能用全称量词量化,例4(不正确) 分析下述推理的正确性,49,56 谓词逻辑的归结推理法,归结方法可推广到谓词逻辑，困难在于出现了量词，变元证明过程同命题逻辑，只不过每一步骤都要考虑到有变元，从而带来复杂性,使用推理规则的推理演算过于灵活，技巧性强，而归结法较为机械，容易使用计算机来实现。,56 谓词逻辑的归结推理法归结方法可推广到谓词逻辑，困难,50,5.6,.,1,谓词逻辑归结证明过程四步骤,(,从例子来理解步骤),(1),为证明,AB,是定理,(A,，,B,为谓词公式,),，即,A,B,等价的是证明,G=A,B,是矛盾式，这是归结法的出发点(反证法),(2),通过,G,的合取形式建立子句集,S,，在建立子句集,S,的时利用前束范式及,Skolem,标准形(不严格)，消去存在量词(以常项代替如,a)，,消去全称量词(注意新的自由变元如,x,y)。,理论：,S,中的前提与,G,在不可满足的意义下是一致的。,5.6.1 谓词逻辑归结证明过程四步骤(从例子来理解步骤,51,(3),对,S,作归结:,(P(x),Q(x),并且(,P(a),R(y),可以归结出,Q(a),R(y),理论：因为(,P(a),Q(a),),(,P(a),R(y),),Q(a),R(y),理论：变元,x,统一换成特定个体,a,称为合一置换,x,a,(4),重复归结方法，最后得到矛盾,(3)对S作归结:,52,562 归结法证明举例,例,1 (,x)(P(x)Q(x)(,x)(Q(x)R(x)=(,x)(P(x)R(x),首先写出公式,G,G,(,x)(P(x)Q(x)(,x)(Q(x)R(x),(,x)(P(x)R(x),为求,G,的子句集,S,，可分别对,(,x)(P(x)Q(x),，,(,x)(Q(x)R(x),，,(,x)(P(x)R(x),作子句集，然后求并集来作为,G,的“子句集”,(,这个“子句集”不一定是,S,，但与,S,同时是不可满足的，而且较,S,来得简单，于是为方便可将这个“子句集”视作,S),(,x)(P(x)Q(x),的子句集为,P(x)VQ(x),(,x)(Q(x)R(x),的子句集为,Q(x)VR(x),(,x)(P(x)R(x),(,x) (P(x)VR(x),(,x)(P(x)R(x),Skolem,化，得子句集,P(a),，,R(a),于是,G,的子句集,S,P(x)VQ(x),，,Q(x)VR(x),，,P(a),，,R(a),562 归结法证明举例例1 (x)(P(x)Q(,53,证明,S,是不可满足的，有归结过程：,(1) P(x)VQ(x),(2) Q(x)VR(x),(3) P(a),(4) R(a),(5) Q(a) (1)(3),归结,(6) R(a) (2)(5),归结,(7),口,(4)(6),归结,证明S是不可满足的，有归结过程：,54,例,2 A,1,(,x)(P(x)(,y)(D(y)L(x,y),A,2,(,x)(P(x)(,y)(Q(y)L(x,，,y),B,(,x)(D(x)Q(x),求证,A,1,A,2,=B,证明 不难建立,A1,的子句集为,P(a),，,D(y)VL(a,，,y),，,A2,的子句集为,P(x)VQ(y)VL(x,，,y), B,的子句集为,D(b),，,Q(b),，求并集得子句集,S,，进而建立归结过程：,例2 A1(x)(P(x)(y)(D(y)L(,55,(1) P(a),(2) D(y)VL(a,，,y),(3) P(x)VQ(y)VL(x,，,y),(4) D(b),(5) Q(b),(6) L(a,，,b) (2)(4),归结,(7) Q(y)VL(a,，,y) (1)(3),归结,(8) L(a,，,b) (5)(7),归结,(9),口,(6)(8),归结,(1) P(a),56,