人工智能-谓词逻辑.pptx

Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,谓词逻辑基础,一阶逻辑,基本概念,个体词：表示主语词,谓词：刻画个体性质或个体之间关系词,量词：表示数量词,人工智能-谓词逻辑,第1页,小王是个工程师。,8,是个自然数。,我去买花。,小丽和小华是朋友。,其中，“小王”、“工程师”、“我”、“花”、“,8”,、“小丽”、“小华”都是个体词，而“是个工程师”、“是个自然数”、“去买”、“是朋友”都是谓词。显然前两个谓词表示是事物性质，第三个谓词“去买”表示一个动作也表示了主、宾两个个体词关系，最终一个谓词“是朋友”表示两个个体词之间关系。,谓词逻辑基础,人工智能-谓词逻辑,第2页,谓词逻辑基础,比如：（,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,活到一百岁以上。,人工智能-谓词逻辑,第3页,一阶逻辑,公式及其解释,个体常量：,a,b,c,个体变量：,x,y,z,谓词符号：,P,Q,R,量词符号：,谓词逻辑基础,人工智能-谓词逻辑,第4页,量词否定等值式：,(,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,）,消去量词等值式：,设个体域为有穷集合（,a,1,a,2,a,n,）,(,x,）,P,（,x,）,P,（,a,1,）,P,（,a,2,）,P,（,a,n,）,(,x,）,P,（,x,）,P,（,a,1,）,P,（,a,2,）,P,（,a,n,）,谓词逻辑基础,人工智能-谓词逻辑,第5页,量词辖域收缩与扩张等值式：,(,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,）,(,Q,P,（,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,）,(,Q,P,（,x,）,),Q,(,x,）,P,（,x,）,谓词逻辑基础,人工智能-谓词逻辑,第6页,谓词逻辑基础,人工智能-谓词逻辑,第7页,SKOLEM,标准形,前束范式,定义,：说公式,A,是一个前束范式，假如,A,中一切量词都位于该公式最左边（不含否定词），且这些量词辖域都延伸到公式末端。,谓词逻辑归结原理,人工智能-谓词逻辑,第8页,即：把全部量词都提到前面去，然后消掉全部量词,(Q,1,x,1,)(Q,2,x,2,),(Q,n,x,n,)M(x,1,x,2,x,n,),约束变项换名规则：,(Qx,）,M,（,x,）,（,Qy,）,M,（,y,）,(Qx,）,M,（,x,z,）,（,Qy,）,M,（,y,z,）,谓词逻辑归结原理,人工智能-谓词逻辑,第9页,量词消去标准：,消去存在量词,“,”,，略去全程量词,“,”,。,注意：,左边有全程量词存在量词，消去时该变量改写成为全程量词函数；如没有，改写成为常量。,谓词逻辑归结原理,人工智能-谓词逻辑,第10页,Skolem,定理,：,谓词逻辑任意公式都能够化为与之等价前束范式，但其前束范式不唯一。,SKOLEM,标准形定义：,消去量词后谓词公式。,注意,：谓词公式,G,SKOLEM,标准形同,G,并不等值,。,谓词逻辑归结原理,人工智能-谓词逻辑,第11页,例：,将下式化为,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),由此得到前述范式,人工智能-谓词逻辑,第12页,第五步，消去“,”（存在量词），略去“,”全称量词,消去,(,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),人工智能-谓词逻辑,第13页,子句与子句集,文字：不含任何连接词谓词公式。,子句：一些文字析取（谓词和）。,子句集,S,求取：,G,SKOLEM,标准形,消去存在变量,以,“,，,”,取代,“,”,，并表示为集合形式。,谓词逻辑归结原理,人工智能-谓词逻辑,第14页,G,是不可满足,S,是不可满足,G,与,S,不等价，但在不可满足得意义下是一致。,定理：,若,G,是给定公式，而,S,是对应子句集，则,G,是不可满足,S,是不可满足。,注意,：,G,真不一定,S,真，而,S,真必有,G,真。,即：,S,=,G,谓词逻辑归结原理,人工智能-谓词逻辑,第15页,G=G,1,G,2,G,3,G,n,子句形,G,字句集能够分解成几个单独处理。,有,S,G,=S,1,U S,2,U S,3,U,U S,n,则,S,G,与,S,1,U S,2,U S,3,U,U S,n,在不可满足得意义上是一致。,即,S,G,不可满足,S,1,U S,2,U S,3,U,U S,n,不可满足,3.3,谓词逻辑归结原理,人工智能-谓词逻辑,第16页,例：对全部,x,y,z,来说，假如,y,是,x,父亲，,z,又是,y,父亲，则,z,是,x,祖父。又知每个人都有父亲，试问对某个人来说谁是它祖父？,求：用一阶逻辑表示这个问题，并建立子句集。,解：这里我们首先引入谓词：,P(x,y),表示,x,是,y,父亲,Q(x,y),表示,x,是,y,祖父,ANS(x),表示问题解答,谓词逻辑归结原理,人工智能-谓词逻辑,第17页,对于第一个条件，“假如,x,是,y,父亲，,y,又是,z,父亲，则,x,是,z,祖父”，一阶逻辑表示式以下：,A,1,：,(,x)(,y)(,z)(P(x,y),P(y,z),Q(x,z),S,A1,：,P(x,y),P(y,z),Q(x,z),对于第二个条件：“每个人都有父亲”，一阶逻辑表示式：,A,2,：,(,y)(,x)P(x,y),S,A2,：,P(f(y),y),对于结论：某个人是它祖父,B,：,(,x)(,y)Q(x,y),否定后得到子句：（,(,x)(,y)Q(x,y),）,ANS(x),S,B,：,Q(x,y),ANS(x),则得到对应子句集为：,S,A1,，,S,A2,，,S,B,谓词逻辑归结原理,人工智能-谓词逻辑,第18页,归结原理正确性根本在于，找到矛盾能够必定不真。,方法：,和命题逻辑一样。,但因为有函数，所以要考虑,合一,和,置换,。,谓词逻辑归结原理,人工智能-谓词逻辑,第19页,置换：能够简单了解为是在一个谓词公式中用置换项去置换变量。,定义：,置换是形如,t,1,/x,1,t,2,/x,2,t,n,/x,n,有限集合。其中，,x,1,x,2,x,n,是互不相同变量，,t,1,t,2,t,n,是不一样于,x,i,项（常量、变量、函数）；,t,i,/x,i,表示用,t,i,置换,x,i,，而且要求,t,i,与,x,i,不能相同，而且,x,i,不能循环地出现在另一个,t,i,中。,比如,a/x,，,c/y,，,f(b)/z,是一个置换。,g(y)/x,，,f(x)/y,不是一个置换，,谓词逻辑归结原理,置换,人工智能-谓词逻辑,第20页,置换合成,设,t,1,/x,1,t,2,/x,2,t,n,/x,n,，,u,1,/y,1,u,2,/y,2,u,n,/y,n,，是两个置换。,则,与,合成也是一个置换，记作,。它是从集合,t,1,/x,1,t,2,/x,2,t,n,/x,n,u,1,/y,1,u,2,/y,2,u,n,/y,n,中删去以下两种元素：,i.,当,t,i,=x,i,时，删去,t,i,/x,i,(i=1,2,n);,Ii.,当,y,i,x,1,x,2,x,n,时，删去,u,j,/y,j,(j=1,2,m),最终剩下元素所组成集合。,合成即是对,t,i,先做,置换然后再做,置换，置换,x,i,谓词逻辑归结原理,人工智能-谓词逻辑,第21页,例：,设：,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,谓词逻辑归结原理,人工智能-谓词逻辑,第22页,合一,合一能够简单地了解为“寻找相对变量置换，使两个谓词公式一致”。,定义：设有公式集,F,F,1,，,F,2,，,，,F,n,，若存在一个置换,，可使,F,1,F,2,=F,n,，则称,是,F,一个合一。同时称,F,1,，,F,2,，,.,，,F,n,是可合一。,例：,设有公式集,F,P(x,y,f(y),P(a,g(x),z),，则,a/x,g(a)/y,f(g(a)/z,是它一个合一。,注意：普通说来，一个公式集合一不是唯一。,谓词逻辑归结原理,人工智能-谓词逻辑,第23页,谓词逻辑归结原理,人工智能-谓词逻辑,第24页,谓词逻辑归结原理,人工智能-谓词逻辑,第25页,谓词逻辑归结原理,人工智能-谓词逻辑,第26页,归结原理,归结注意事项：,谓词一致性,，,P(),与,Q(),，不能够,常量一致性，,P(a,),与,P(b,.),，不能够,变量，,P(a,.),与,P(x,),，能够,变量与函数，,P(a,x,.),与,P(x,f(x),),，不能够；,是不能同时消去两个互补对，,PQ,与,P,Q,空，不能够,先进行内部简化（置换、合并）,谓词逻辑归结原理,人工智能-谓词逻辑,第27页,归结过程,写出谓词关系公式,用反演法写出谓词表示式,SKOLEM,标准形,子句集,S,对,S,中可归结子句做归结,归结式仍放入,S,中，重复归结过程,得到空子句,得证,谓词逻辑归结原理,人工智能-谓词逻辑,第28页,例题,“高兴学生”问题,假设任何经过计算机考试并获奖人都是高兴，任何肯学习或幸运人都能够经过全部考试，张不愿学习但他是幸运，任何幸运人都能获奖。求证：张是高兴。,解：先将问题用谓词表示以下：,R1:“,任何经过计算机考试并获奖人都是高兴”,(,x)(Pass(x,computer)Win(x,prize)Happy(x),R2:“,任何肯学习或幸运人都能够经过全部考试”,(,x)(,y)(Study(x)Lucky(x)Pass(x,y),R3:“,张不愿学习但他是幸运”,Study(zhang)Lucky(zhang),R4:“,任何幸运人都能获奖”,(,x)(Luck(x)Win(x,prize),结论：“张是高兴”否定,Happy(zhang),人工智能-谓词逻辑,第29页,例题,“高兴学生”问题,由,R1,及逻辑转换公式,:PWH=,（,PW,）,H,，可得,(1),Pass(x,computer),Win(x,prize)Happy(x),由,R2,：,(2),Study(y)Pass(y,z),(3),Lucky(u)Pass(u,v),由,R3,：,(4),Study(zhang),(5)Lucky(zhang),由,R4,：,(6),Lucky(w)Win(w,，,prize),由结论：,(7),Happy(zhang),（结论否定）,(8),Pass(w,computer)Happy(w),Luck(w)(1)(6),，,w/x,(9),Pass(zhang,computer),Lucky(zhang)(8)(7),，,zhang/w,(10),Pass(zhang,computer)(9)(5),(11),Lucky(zhang)(10)(3),，,zhang/u,computer/v,(12),(11)(5),人工智能-谓词逻辑,第30页,归结法实质：,归结法是仅有一条推理规则推理方法。,归结过程是一个语义树坍毁过程。,归结法问题,子句中有等号或不等号时，完备性不成立。,Herbrand,定理不实用性引出了可实用归结法。,谓词逻辑归结原理,人工智能-谓词逻辑,第31页,归结过程控制策略,要处理问题：,归结方法知识爆炸。,控制策略目标,归结点尽可能少,控制策略标准,给出控制策略，以使仅对选择适当子句间方可做归结。防止多出、无须要归结式出现。或者说，少做些归结仍能导出空子句。,谓词逻辑归结原理,人工智能-谓词逻辑,第32页,删除策略,=,完备,名词解释：归类：设有两个子句,C,和,D,，若有置换,使得,C,D,成立，则称子句,C,把子句,D,归类。,因为小能够代表大，所以小吃掉大了。,若对,S,使用归结推理过程中，当归结式,C,j,是重言式（永真式）和,C,j,被,S,中子句和子句集归结式,C,i,(ij),所归类时，便将,C,j,删除。这么推理过程便称做使用了删除策略归结过程。,谓词逻辑归结原理,人工智能-谓词逻辑,第33页,主要思想：归结过程在寻找可归结子句时，子句集中子句越多，需要付出代价就会越大。假如在归结时能把子句集中无用子句删除掉，就会缩小搜索范围，降低比较次数，从而提升归结效率。删除策略对阻止无须要归结式产生来缩短归结过程是有效。然而要在归结式,C,j,产生后方能判别它是否可被删除，这部分计算量是要花费，只是节约了被删除子句又生成归结式。尽管使用删除策略归结，少做了归结但不影响产生空子句，就是说删除策略归结推理是完备。,谓词逻辑归结原理,人工智能-谓词逻辑,第34页,采取支撑集,完备,支撑集：设有不可满足子句集,S,子集,T,，假如,S-T,是可满足，则,T,是支持集。,采取支撑集策略时，从开始到得到,整个归结过程中，只选取不一样时属于,S-T,子句，在其间进行归结。就是说，最少有一个子句来自于支撑集,T,或由,T,导出归结式。,谓词逻辑归结原理,人工智能-谓词逻辑,第35页,比如：,A,1,A,2,A,3,B,中,B,能够作为支撑集使用。要求每一次参加归结亲本子句中，只要应该有一个是有目标公式否定（,B,）所得到子句或者它们后代。,支撑集策略归结是完备，一样，全部可归结谓词公式都能够用采取支撑集策略到达加紧归结速度目标。问题是怎样寻找适当支撑集。一个最轻易找到支撑集是目标子句非，即,S,B,。,谓词逻辑归结原理,人工智能-谓词逻辑,第36页,S,T,可满足,支撑集示意图,谓词逻辑归结原理,人工智能-谓词逻辑,第37页,语义归结,完备,语义归结策略是将子句,S,按照一定语义分成两部分，约定每部分内子句间不允许作归结。同时还引入了文字次序，约定归结时其中一个子句被归结文字只能是该子句中,“,最大,”,文字。,语义归结策略归结是完备，一样，全部可归结谓词公式都能够用采取语义归结策略到达加紧归结速度目标。问题是怎样寻找适当语义分类方法，并依据其含义将子句集两个部分中子句进行排序。,谓词逻辑归结原理,人工智能-谓词逻辑,第38页,线性归结,完备,线性归结策略首先从子句集中选取一个称作顶子句子句,C,0,开始作归结。归结过程中所得到归结式,C,i,马上同另一子句,B,i,进行归结得归结式,C,i+1,。而,B,i,属于,S,或是已出现归结式,C,j,(j,完备,单元归结策略要求在归结过程中，每次归结都有一个子句是单元子句（只含一个文字子句）或单元因子。显而易见，词中方法能够简单地削去另一个非单子句中一个因子，使其长度降低，组成简单化，归结效率较高。,初始子句集中没有单元子句时，单元归结策略无效。所以说,“,反之不成立,”,，即此问题不能采取单元归结策略,。,人工智能-谓词逻辑,第41页,输入归结,=,完备,与单元归结策略相同，输入归结策略要求在归结过程中，每一次归结两个子句中必须有一个是,S,原始子句。这么能够防止归结出无须要新子句加入归结，造成恶性循环。能够降低无须要归结次数。,人工智能-谓词逻辑,第42页,如同单元归结策略，不是全部可归结谓词公式最终结论都是能够从原始子句集中得到。简单例子，归结结束时，即最终一个归结式为空子句条件是，参加归结双方必须是两个单元子句。原始子句集中没有单元子句谓词公式一定不能采取输入归结策略。,人工智能-谓词逻辑,第43页,