人工智能-谓词逻辑43

,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,#,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,#,谓词逻辑基础,一阶逻辑,基本概念,个体词：表示主语的词,谓词：刻画个体性质或个体之间关系的词,量词：表示数量的词,小王是,个,个工程,师,师。,8是个自,然,然数。,我去买,花,花。,小丽和,小,小华是,朋,朋友。,其中，,“,“小王,”,”、“,工,工程师,”,”、“,我,我”、,“,“花”,、,、“8”、“小,丽,丽”、,“,“小华,”,”都是,个,个体词,，,，而“,是,是个工,程,程师”,、,、“是,个,个自然,数,数”、,“,“去买,”,”、“,是,是朋友,”,”都是,谓,谓词。,显,显然前,两,两个谓,词,词表示,的,的是事,物,物的性,质,质，第,三,三个谓,词,词“去,买,买”表,示,示的一,个,个动作,也,也表示,了,了主、,宾,宾两个,个,个体词,的,的关系,，,，最后,一,一个谓,词,词“是,朋,朋友”,表,表示两,个,个个体,词,词之间,的,的关系,。,。,谓词逻,辑,辑基础,谓词逻,辑,辑基础,例如：,（,（1）所有,的,的人都,是,是要死,的,的。,（2）有的人,活,活到一,百,百岁以,上,上。,在个体,域,域D为人类,集,集合时,，,，可符,号,号化为,：,：,（1）xP(x)，其中P(x)表示x是要死,的,的。,（2）x Q(x),其中Q(x)表示x活到一,百,百岁以,上,上。,在个体,域,域D是全总,个,个体域,时,时，,引入特,殊,殊谓词R(x)表示x是人，,可,可符号,化,化为：,（1）x（R(x)P(x)）,其中，R(x)表示x是人；P(x)表示x是要死,的,的。,（2）x（R(x)Q(x)），,其中，R(x)表示x是人；Q(x)表示x活到一,百,百岁以,上,上。,一阶逻,辑,辑,公式及,其,其解释,个体常,量,量：a,b,c,个体变,量,量：x,y,z,谓词符,号,号：P,Q,R,量词符,号,号：,谓词逻,辑,辑基础,量词否,定,定等值,式,式：,(x）P（x）,（y）P（y）,(x）P（x）,（y）P（y）,量词分,配,配等值,式,式：,(x）(P（x）,Q（x）),(,(x）P（x）,(x）Q（x）,(,x）(P（x）,Q（x）),(,(,x）P（x）,(,x）Q（x）,消去量,词,词等值,式,式：,设个体,域,域为有,穷,穷集合,（,（a1,a2,an）,(x）P（x）P（a1）,P（a2）,P（an）,(,x）P（x）P（a1）,P（a2）,P（an）,谓词逻,辑,辑基础,量词辖,域,域收缩,与,与扩张,等,等值式,：,：,(x）(P（x）Q),(,(x）P（x）Q,(x）(P（x）,Q),(,(x）P（x）,Q,(x）(P（x）Q),(,(x）P（x）Q,(x）(QP（x）)Q(x）P（x）,(x）(P（x）Q),(,(x）P（x）Q,(x）(P（x）,Q),(,(x）P（x）,Q,(x）(P（x）Q),(,(x）P（x）Q,(x）(QP（x）)Q(x）P（x）,谓词逻,辑,辑基础,谓词逻,辑,辑基础,SKOLEM标准形,前束范,式,式,定义：说公,式,式A是一个,前,前束范,式,式，如,果,果A中的一,切,切量词,都,都位于,该,该公式,的,的最左,边,边（不,含,含否定,词,词），,且,且这些,量,量词的,辖,辖域都,延,延伸到,公,公式的,末,末端。,谓词逻,辑,辑归结,原,原理,即：,把,把所有,的,的量词,都,都提到,前,前面去,，,，然后,消,消掉所,有,有量词,(Q1x1)(Q2x2)(Qnxn)M(x1,x2,xn),约束变,项,项换名,规,规则：,(Qx）M（x）,（Qy）M（y）,(Qx）M（x,z）,（Qy）M（y,z）,谓词逻,辑,辑归结,原,原理,量词消,去,去原则,：,：,消去存,在,在量词“”，略去,全,全程量,词,词“”。,注意：,左边有,全,全程量,词,词的存,在,在量词,，,，消去,时,时该变,量,量改写,成,成为全,程,程量词,的,的函数,；,；如没,有,有，改,写,写成为,常,常量。,谓词逻,辑,辑归结,原,原理,Skolem定理：,谓词逻,辑,辑的任,意,意公式,都,都可以,化,化为与,之,之等价,的,的前束,范,范式，,但,但其前,束,束范式,不,不唯一,。,。,SKOLEM标准形,定,定义：,消去量,词,词后的,谓,谓词公,式,式。,注意：谓词,公,公式G的SKOLEM标准形,同,同G并不等,值,值。,谓词逻,辑,辑归结,原,原理,例：将下式,化,化为Skolem标准形,：,：,(x)(y)P,(,(a,x,y)(x)(y)Q,(,(y,b)R(x,),),解：第,一,一步，,消,消去号，得,：,：,(x)(y)P,(,(a,x,y),),)(x),(,(y)Q,(,(y,b)R(x,),),第二步,，,，深,入,入到量,词,词内部,，,，得：,(x)(y)P,(,(a,x,y)(x)(y)Q,(,(y,b)R(x,),),第三步,，,，变元,易,易名，,得,得,(x)(y)P,(,(a,x,y)(u)(v)(Q,(,(v,b)R(u,),),第四步,，,，存在,量,量词左,移,移，直,至,至所有,的,的量词,移,移到前,面,面，(x),(,(y),(,(u)(v)(P(a,x,y,),)(Q(v,b)R(u,),),由此得,到,到前述,范,范式,第五步,，,，消去,“,“”（存,在,在量词,）,），略,去,去“”全称,量,量词,消去(y)，因为,它,它左边,只,只有(x)，所以,使,使用x的函数f(x,),)代替之,，,，这样,得,得到：,(x)(u),(v),(P(a,x,f(x,),),Q(v,b,),),R(u,),),消去(u)，同理,使,使用g(x,),)代替之,，,，这样,得,得到：,(x),(v),(P,(,(a,x,f(x),Q(v,b,),),R(g,(,(x),),),则，略,去,去全称,变,变量，,原,原式的Skolem标准形,为,为：,P(a,x,f,(,(x),),),Q(v,b,),),R(g,(,(x),),),子句与,子,子句集,文字：,不,不含任,何,何连接,词,词的谓,词,词公式,。,。,子句：,一,一些文,字,字的析,取,取（谓,词,词的和,）,）。,子句集S的求取,：,：,G SKOLEM标准形,消,去,去存在,变,变量,以“，”取代“,”，并表,示,示为集,合,合形式,。,。,谓词逻,辑,辑归结,原,原理,G是不可,满,满足的,S是不可,满,满足的,G与S不等价,，,，但在,不,不可满,足,足得意,义,义下是,一,一致的,。,。,定理：,若G是给定,的,的公式,，,，而S是相应,的,的子句,集,集，则G是不可,满,满足的,S是不可,满,满足的,。,。,注意：G真不一,定,定S真，而S真必有G真。,即：S,=,G,谓词逻,辑,辑归结,原,原理,G=G1 G2 G3 Gn的子句,形,形,G的字句,集,集可以,分,分解成,几,几个单,独,独处理,。,。,有SG=S1U S2U S3UU Sn,则SG与S1U S2U S3UU Sn在不可,满,满足得,意,意义上,是,是一致,的,的。,即SG不可满,足,足S1U S2U S3UU Sn不可满,足,足,3.3谓词逻,辑,辑归结,原,原理,例：对,所,所有的x,y,z来说，,如,如果y是x的父亲,，,，z又是y的父亲,，,，则z是x的祖父,。,。又知,每,每个人,都,都有父,亲,亲，试,问,问对某,个,个人来,说,说谁是,它,它的祖,父,父？,求：用,一,一阶逻,辑,辑表示,这,这个问,题,题，并,建,建立子,句,句集。,解：这,里,里我们,首,首先引,入,入谓词,：,：,P(x,y,),)表示x是y的父亲,Q(x,y,),)表示x是y的祖父,ANS,(,(x)表示问,题,题的解,答,答,谓词逻,辑,辑归结,原,原理,对于第,一,一个条,件,件，“,如,如果x是y的父亲,，,，y又是z的父亲,，,，则x是z的祖父,”,”，一,阶,阶逻辑,表,表达式,如,如下：,A1：(x)(y)(z)(P(x,y,),)P(y,z,),)Q(x,z,),),SA1：P(x,y,),)P(y,z,),)Q(x,z,),),对于第,二,二个条,件,件：“,每,每个人,都,都有父,亲,亲”，,一,一阶逻,辑,辑表达,式,式：,A2：(y)(x)P,(,(x,y),SA2：P(f,(,(y),y,),),对于结,论,论：某,个,个人是,它,它的祖,父,父,B：(x)(y)Q,(,(x,y),否定后,得,得到子,句,句：,（(x)(y)Q,(,(x,y)）ANS,(,(x),SB：Q(x,y,),)ANS,(,(x),则得到,的,的相应,的,的子句,集,集为：SA1，SA2，SB,谓词逻,辑,辑归结,原,原理,归结原,理,理正确,性,性的根,本,本在于,，,，找到,矛,矛盾可,以,以肯定,不,不真。,方法：,和命题,逻,逻辑一,样,样。,但由于,有,有函数,，,，所以,要,要考虑合一和置换。,谓词逻,辑,辑归结,原,原理,置换：,可,可以简,单,单的理,解,解为是,在,在一个,谓,谓词公,式,式中用,置,置换项,去,去置换,变,变量。,定义：,置换是,形,形如t1/x1,t2/x2,tn/xn的有限,集,集合。,其,其中，x1,x2,xn是互不,相,相同的,变,变量，t1,t2,tn是不同,于,于xi的项（,常,常量、,变,变量、,函,函数）,；,；ti/xi表示用ti置换xi，并且,要,要求ti与xi不能相,同,同，而,且,且xi不能循,环,环地出,现,现在另,一,一个ti中。,例如,a/x，c/y，f(b,),)/z,是一个,置,置换。,g(y)/x，f(x,),)/y,不是一,个,个置换,，,，,谓词逻,辑,辑归结,原,原理,置换,置换的,合,合成,设t1/x1,t2/x2,tn/xn，,u1/y1,u2/y2,un/yn，是两,个,个置换,。,。,则与的合成,也,也是一,个,个置换,，,，记作。它是,从,从集合,t1/x1,t2/x2,tn/xn,u1/y1,u2/y2,un/yn,中删去,以,以下两,种,种元素,：,：,i.,当ti=xi时，删,去,去ti/xi(i,=,=1,2,n,),);,Ii.,当yix1,x2,xn时，删,去,去uj/yj(j,=,=1,2,m,),),最后剩,下,下的元,素,素所构,成,成的集,合,合。,合成即,是,是对ti先做置换然,后,后再做置换，,置,置换xi,谓词逻,辑,辑归结,原,原理,例：,设：f(y)/x,z/y,，a/x,b/y,y,/,/z，求与的合成,。,。,解：先,求,求出集,合,合,f(b/y,),)/x,(y/z,),)/y,a,/,/x,b/y,y/z,f(b)/x,y/y,a,/,/x,b/y,y/z,其中，f(b,),)/x中的f(b,),)是置换作用于f(y,),)的结果,；,；y/y中的y是置换作用于z的结果,。,。在该,集,集合中,，,，y/y满足定,义,义中的,条,条件i，需要,删,删除；a/x，b/y满足定,义,义中的,条,条件ii，也需,要,要删除,。,。最后,得,得,f(b)/x，y/z,谓词逻,辑,辑归结,原,原理,合一,合一可,以,以简单,地,地理解,为,为“寻,找,找相对,变,变量的,置,置换，,使,使两个,谓,谓词公,式,式一致,”,”。,定义：,设,设有公,式,式集FF1，F2，Fn，若存,在,在一个,置,置换，可使F1F2=Fn，则称是F的一个,合,合一。,同,同时称F1，F2，.，Fn是可合,一,一的。,例：,设有公,式,式集FP(x,y,f(y,),),P(a,g,(,(x),z),，则a/x,g(a,),)/y,f,(,(g(a),/,/z是它的,一,一个合,一,一。,注意：,一,一