谓词逻辑基础优秀PPT.ppt

3.2谓词逻辑基础谓词逻辑基础一阶逻辑一阶逻辑l基本概念基本概念l个体词：表示主语的词个体词：表示主语的词l谓词：刻画个体性质或个体之间关系的词谓词：刻画个体性质或个体之间关系的词l量词：表示数量的词量词：表示数量的词l小王是个工程师。小王是个工程师。l8是个自然数。是个自然数。l我去买花。我去买花。l小丽和小华是挚友。小丽和小华是挚友。l其其中中，“小小王王”、“工工程程师师”、“我我”、“花花”、“8”、“小小丽丽”、“小小华华”都都是是个个体体词词，而而“是是个个工工程程师师”、“是是个个自自然然数数”、“去去买买”、“是是挚挚友友”都都是是谓谓词词。明明显显前前两两个个谓谓词词表表示示的的是是事事物物的的性性质质，第第三三个个谓谓词词“去去买买”表表示示的的一一个个动动作作也也表表示示了了主主、宾宾两两个个个个体体词词的的关关系系，最最终终一一个个谓谓词词“是是挚挚友友”表表示示两两个个个个体体词词之之间间的关系。的关系。3.2谓词逻辑基础谓词逻辑基础3.2谓词逻辑基础谓词逻辑基础l例如：（例如：（1）全部的人都是要死的。）全部的人都是要死的。l（2）有的人活到一百岁以上。有的人活到一百岁以上。l在个体域在个体域D为人类集合时，可符号化为：为人类集合时，可符号化为：l（1）xP(x)，其中，其中P(x)表示表示x是要死的。是要死的。l（2）xQ(x),其中其中Q(x)表示表示x活到一百岁以上。活到一百岁以上。l在个体域在个体域D是全总个体域时，是全总个体域时，l引入特殊谓词引入特殊谓词R(x)表示表示x是人，可符号化为：是人，可符号化为：l（1）x（R(x)P(x)）,l其中，其中，R(x)表示表示x是人；是人；P(x)表示表示x是要死的。是要死的。l（2）x（R(x)Q(x)），），l其中，其中，R(x)表示表示x是人；是人；Q(x)表示表示x活到一百岁以上。活到一百岁以上。一阶逻辑一阶逻辑公式及其说明公式及其说明个体常量：个体常量：a,b,c个体变量：个体变量：x,y,z谓词符号：谓词符号：P,Q,R量词符号：量词符号：,3.2谓词逻辑基础谓词逻辑基础量词否定等值式：量词否定等值式：(x x）P P（x x）（y y）P P（y y）(x x）P P（x x）（y y）P P（y y）量词安排等值式：量词安排等值式：(x x）(P(P（x x）Q Q（x x）)()(x x）P P（x x）(x x）Q Q（x x）(x x）(P(P（x x）Q Q（x x）)()(x x）P P（x x）(x x）Q Q（x x）消去量词等值式：设个体域为有穷集合（消去量词等值式：设个体域为有穷集合（a1,a2,a1,a2,anan）(x x）P P（x x）P P（a1 a1）P P（a2 a2）P P（an an）(x x）P P（x x）P P（a1 a1）P P（a2 a2）P P（an an）3.2谓词逻辑基础谓词逻辑基础量词辖域收缩与扩张等值式：量词辖域收缩与扩张等值式：l(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Ql(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Q l(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Q l(x x ）(Q Q P P（x x）)Q Q (x x ）P P（x x）l(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Ql(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Q l(x x ）(P P（x x）Q Q)()(x x ）P P（x x）Q Q l(x x ）(Q Q P P（x x）)Q Q (x x ）P P（x x）3.2谓词逻辑基础谓词逻辑基础3.2谓词逻辑基础谓词逻辑基础SKOLEMSKOLEM标准形标准形前束范式前束范式定定义义：说说公公式式A A是是一一个个前前束束范范式式，假假如如A A中中的的一一切切量量词词都都位位于于该该公公式式的的最最左左边边（不不含含否否定定词词），且且这这些些量量词词的的辖辖域域都都延长到公式的末端。延长到公式的末端。3.3谓词逻辑归结原理谓词逻辑归结原理即：即：把全部的量词都提到前面去，然后消把全部的量词都提到前面去，然后消掉全部量词掉全部量词(Q1x1)(Q2x2)(Qnxn)M(x1,x2,xn)(Q1x1)(Q2x2)(Qnxn)M(x1,x2,xn)约束变项换名规则：约束变项换名规则：(Qx(Qx）M M（x x）（Qy Qy）M M（y y）(Qx(Qx）M M（x,zx,z）（Qy Qy）M M（y,zy,z）3.3谓词逻辑归结原理谓词逻辑归结原理 量词消去原则：量词消去原则：消去存在量词消去存在量词“”，略去全程量词，略去全程量词“”。留意：左边有全程量词的存在量词，留意：左边有全程量词的存在量词，消去时该变量改写成为全程量词的函消去时该变量改写成为全程量词的函数；如没有，改写成为常量。数；如没有，改写成为常量。3.3谓词逻辑归结原理谓词逻辑归结原理 SkolemSkolem定理：定理：谓词逻辑的随意公式都可以化为与之等价的前束范式，但其前束范式不唯一。谓词逻辑的随意公式都可以化为与之等价的前束范式，但其前束范式不唯一。SKOLEMSKOLEM标准形定义：标准形定义：消去量词后的谓词公式。消去量词后的谓词公式。留意：谓词公式留意：谓词公式G G的的SKOLEMSKOLEM标准形同标准形同G G并不等值。并不等值。3.3谓词逻辑归结原理谓词逻辑归结原理例：例：将下式化为将下式化为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)由此得到前述范式由此得到前述范式l第第五五步步，消消去去“”（存存在在量量词词），略略去去“”全全称称量词量词l消消去去(y)，因因为为它它左左边边只只有有(x)，所所以以运运用用x的的函函数数f(x)代替之，这样得到：代替之，这样得到：l(x)(u)(v)(P(a,x,f(x)Q(v,b)R(u)l消去消去(u)，同理运用，同理运用g(x)代替之，这样得到：代替之，这样得到：l(x)(v)(P(a,x,f(x)Q(v,b)R(g(x)l则，略去全称变量，原式的则，略去全称变量，原式的Skolem标准形为：标准形为：lP(a,x,f(x)Q(v,b)R(g(x)l子句与子句集子句与子句集l文字：不含任何连接词的谓词公式。文字：不含任何连接词的谓词公式。l子句：一些文字的析取（谓词的和）。子句：一些文字的析取（谓词的和）。l子句集子句集S S的求取：的求取：G G SKOLEM SKOLEM标准形标准形 消去存在变量消去存在变量 以以“，”取代取代“”，并表示为集合形式，并表示为集合形式 。3.3谓词逻辑归结原理谓词逻辑归结原理l G G是不行满足的是不行满足的 S S是不行满足的是不行满足的lG G与与S S不等价，但在不行满足得意义下是一样的。不等价，但在不行满足得意义下是一样的。l定理：定理：l若若G G是给定的公式，而是给定的公式，而S S是相应的子句集，则是相应的子句集，则G G是不是不行满足的行满足的 S S是不行满足的。是不行满足的。l l留意：留意：G G真不确定真不确定S S真，而真，而S S真必有真必有G G真。真。l即：即：S=G S=G3.3谓词逻辑归结原理谓词逻辑归结原理lG=G1 G2 G3 Gn G=G1 G2 G3 Gn 的子句形的子句形lG G的字句集可以分解成几个单独处理。的字句集可以分解成几个单独处理。l l有有 SG=S1 U S2 U S3 U U Sn SG=S1 U S2 U S3 U U Snl则则SG SG 与与 S1 U S2 U S3 U U Sn S1 U S2 U S3 U U Sn在不行满在不行满足得意义上是一样的。足得意义上是一样的。l即即SG SG 不行满足不行满足 S1 U S2 U S3 U U S1 U S2 U S3 U U SnSn不行满足不行满足3.3谓词逻辑归结原理谓词逻辑归结原理例例：对对全全部部的的x,y,z来来说说，假假如如y是是x的的父父亲亲，z又又是是y的的父父亲亲，则则z是是x的的祖祖父父。又又知知每每个个人人都都有有父父亲亲，试试问问对对某某个人来说谁是它的祖父？个人来说谁是它的祖父？求：用一阶逻辑表示这个问题，并建立子句集。求：用一阶逻辑表示这个问题，并建立子句集。解：这里我们首先引入谓词：解：这里我们首先引入谓词：P(x,y)表示表示x是是y的父亲的父亲Q(x,y)表示表示x是是y的祖父的祖父ANS(x)表示问题的解答表示问题的解答3.3谓词逻辑归结原理谓词逻辑归结原理对对于于第第一一个个条条件件，“假假如如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，SB3.3谓词逻辑归结原理谓词逻辑归结原理l归结原理正确性的根本在于，找到冲突归结原理正确性的根本在于，找到冲突可以确定不真。可以确定不真。l方法：方法：l和命题逻辑一样。和命题逻辑一样。l但由于有函数，所以要考虑合一和置换。但由于有函数，所以要考虑合一和置换。l3.3谓词逻辑归结原理谓词逻辑归结原理l置置换换：可可以以简简洁洁的的理理解解为为是是在在一一个个谓谓词词公公式式中中用用置置换换项项去去置置换换变变量。量。l定义：定义：l置置换换是是形形如如t1/x1,t2/x2,tn/xn的的有有限限集集合合。其其中中，x1,x2,xn是是互互不不相相同同的的变变量量，t1,t2,tn是是不不同同于于xi的的项项（常常量量、变变量量、函函数数）；ti/xi表表示示用用ti置置换换xi，并并且且要要求求ti与与xi不不能能相相同同，而而且且xi不能循环地出现在另一个不能循环地出现在另一个ti中。中。l例如例如la/x，c/y，f(b)/z是一个置换。是一个置换。lg(y)/x，f(x)/y不是一个置换，不是一个置换，3.3谓词逻辑归结原理谓词逻辑归结原理置换置换置换的合成置换的合成l设设t1/x1,t2/x2,tn/xn，l u1/y1,u2/y2,un/yn，是两个置换。，是两个置换。l则则与与 的合成也是一个置换，记作的合成也是一个置换，记作。它是从集合。它是从集合lt1/x1,t2/x2,tn/xn,u1/y1,u2/y2,un/ynl中删去以下两种元素：中删去以下两种元素：li.当当ti=xi时，删去时，删去ti/xi(i=1,2,n);lIi.当当yix1,x2,xn时，删去时，删去uj/yj(j=1,2,m)l最终剩下的元素所构成的集合。最终剩下的元素所构成的集合。l合成即是对合成即是对ti先做先做 置换然后再做置换然后再做置换，置换置换，置换xi3.3谓词逻辑归结原理谓词逻辑归结原理l例：例：l设设：f(y)/x,z/y，a/x,b/y,y/z，求求与与 的的合合成。成。l解：先求出集合解：先求出集合lf(b/y)/x,(y/z)/y,a/x,b/y,y/zf(b)/x,y/y,a/x,b/y,y/zl其其中中，f(b)/x中中的的f(b)是是置置换换 作作用用于于f(y)的的结结果果；y/y中中的的y是是置置换换 作作用用于于z的的结结果果。在在该该集集合合中中，y/y满满足足定定义义中中的的条条件件i，须须要要删删除除；a/x，b/y满满足足定定义义中中的的条条件件ii，也也须须要要删除。最终得删除。最终得l f(b)/x，y/z3.3谓词逻辑归结原理谓词逻辑归结原理合一合一l合合一一可可以以简简洁洁地地理理解解为为“找找寻寻相相对对变变量量的的置置换换，使使两两个个谓谓词词公式一样公式一样”。l定定义义：设设有有公公式式集集FF1，F2，Fn，若若存存在在一一个个置置换换，可可使使F1F2=Fn，则则称称是是F的的一一个个合合一一。同时称同时称F1，F2，.，Fn是可合一的。是可合一的。l例：例：l设设有有公公式式集集FP(x,y,f(y),P(a,g(x),z)，则则 a/x,g(a)/y,f(g(a)/z是它的一个合一。是它的一个合一。l留意：一般说来，一个公式集的合一不是唯一的。留意：一般说来，一个公式集的合一不是唯一的。3.3谓词逻辑归结原理谓词逻辑归结原理3.3谓词逻辑归结原理谓词逻辑归结原理3.3谓词逻辑归结原理谓词逻辑归结原理3.3谓词逻辑归结原理谓词逻辑归结原理归结原理归结原理l归结的留意事项：归结的留意事项：l谓词的一样性，谓词的一样性，P()与与Q()，不行以不行以l常量的一样性，常量的一样性，P(a,)与与P(b,.)，不行不行以以l变量，变量，P(a,.)与与P(x,)，可以可以l变量与函数，变量与函数，P(a,x,.)与与P(x,f(x),)，不行以；不行以；l是不能同时消去两个互补对，是不能同时消去两个互补对，PQ与与PQ的空，不行以的空，不行以l先进行内部简化（置换、合并）先进行内部简化（置换、合并）3.3谓词逻辑归结原理谓词逻辑归结原理l归结的过程归结的过程写出谓词关系公式写出谓词关系公式 用反演法写出谓词表达式用反演法写出谓词表达式 SKOLEMSKOLEM标准形标准形 子句集子句集S S 对对S S中可归结的子句做归结中可归结的子句做归结 归结式仍放入归结式仍放入S S中，反复归结过程中，反复归结过程 得到空子句得到空子句 得证得证3.3谓词逻辑归结原理谓词逻辑归结原理例题例题“快乐学生快乐学生”问题问题l假假设设任任何何通通过过计计算算机机考考试试并并获获奖奖的的人人都都是是快快乐乐的的，任任何何肯肯学学习习或或幸幸运运的的人人都都可可以以通通过过全全部部的的考考试试，张张不不愿愿学学习习但但他他是是幸幸运运的的，任任何何幸幸运运的的人人都都能能获获奖奖。求求证证：张是快乐的。张是快乐的。l解：先将问题用谓词表示如下：解：先将问题用谓词表示如下：lR1:“任何通过计算机考试并获奖的人都是快乐的任何通过计算机考试并获奖的人都是快乐的”l(x)(Pass(x,computer)Win(x,prize)Happy(x)lR2:“任何肯学习或幸运的人都可以通过全部考试任何肯学习或幸运的人都可以通过全部考试”l(x)(y)(Study(x)Lucky(x)Pass(x,y)lR3:“张不愿学习但他是幸运的张不愿学习但他是幸运的”lStudy(zhang)Lucky(zhang)lR4:“任何幸运的人都能获奖任何幸运的人都能获奖”l(x)(Luck(x)Win(x,prize)l结论：结论：“张是快乐的张是快乐的”的否定的否定lHappy(zhang)例题例题“快乐学生快乐学生”问题问题l由由R1及逻辑转换公式及逻辑转换公式:PWH=（PW）H，可得，可得l(1)Pass(x,computer)Win(x,prize)Happy(x)l由由R2：(2)Study(y)Pass(y,z)l(3)Lucky(u)Pass(u,v)l由由R3：(4)Study(zhang)l(5)Lucky(zhang)l由由R4：(6)Lucky(w)Win(w，prize)l由结论：由结论：(7)Happy(zhang)（结论的否定）（结论的否定）l(8)Pass(w,computer)Happy(w)Luck(w)(1)(6)，w/xl(9)Pass(zhang,computer)Lucky(zhang)(8)(7)，zhang/wl(10)Pass(zhang,computer)(9)(5)l(11)Lucky(zhang)(10)(3)，zhang/u,computer/vl(12)(11)(5)l归结法的实质：归结法的实质：l归结法是仅有一条推理规则的推理方法。归结法是仅有一条推理规则的推理方法。l归结的过程是一个语义树倒塌的过程。归结的过程是一个语义树倒塌的过程。l归结法的问题归结法的问题l子句中有等号或不等号时，完备性不成立。子句中有等号或不等号时，完备性不成立。lHerbrand定理的不好用性引出了可好用定理的不好用性引出了可好用的归结法。的归结法。3.3谓词逻辑归结原理谓词逻辑归结原理归结过程的限制策略归结过程的限制策略l要解决的问题：要解决的问题：l归结方法的学问爆炸。归结方法的学问爆炸。l限制策略的目的限制策略的目的l归结点尽量少归结点尽量少l限制策略的原则限制策略的原则l给出限制策略，以使仅对选择合适的子给出限制策略，以使仅对选择合适的子句间方可做归结。避开多余的、不必要句间方可做归结。避开多余的、不必要的归结式出现。或者说，少做些归结仍的归结式出现。或者说，少做些归结仍能导出空子句。能导出空子句。3.3谓词逻辑归结原理谓词逻辑归结原理删除策略=完备名词说明：归类：设有两个子句C和D，若有置换使得C D成立，则称子句C把子句D归类。由于小的可以代表大的，所以小的吃掉大的了。若对S运用归结推理过程中，当归结式Cj是重言式（永真式）和Cj被S中子句和子句集的归结式Ci(ij)所归类时，便将Cj删除。这样的推理过程便称做运用了删除策略的归结过程。3.3谓词逻辑归结原理谓词逻辑归结原理l主主要要思思想想：归归结结过过程程在在找找寻寻可可归归结结子子句句时时，子子句句集集中中的的子子句句越越多多，须须要要付付出出的的代代价价就就会会越越大大。假假如如在在归归结结时时能能把把子子句句集集中中无无用用的的子子句句删删除除掉掉，就就会会缩缩小小搜搜寻寻范范围围，削削减减比比较较次次数数，从从而而提提高高归归结结效效率率。删删除除策策略略对对阻阻挡挡不不必必要要的的归归结结式式的的产产生生来来缩缩短短归归结结过过程程是是有有效效的的。然然而而要要在在归归结结式式CjCj产产生生后后方方能能判判别别它它是是否否可可被被删删除除，这这部部分分计计算算量量是是要要花花费费的的，只只是是节节约约了了被被删删除除的的子子句句又又生生成成的的归归结结式式。尽尽管管运运用用删删除除策策略略的的归归结结，少少做做了了归归结结但但不不影影响响产产生生空空子子句句，就就是是说说删删除除策略的归结推理是完备的。策略的归结推理是完备的。3.3谓词逻辑归结原理谓词逻辑归结原理接受支撑集接受支撑集 完备完备 支撑集：设有不行满足子句集支撑集：设有不行满足子句集S S的子的子集集T T，假如，假如S-TS-T是可满足的，则是可满足的，则T T是是支持集。支持集。接受支撑集策略时，从起先到得到接受支撑集策略时，从起先到得到 的整个归结过程中，只选取不同的整个归结过程中，只选取不同时属于时属于S-TS-T的子句，在其间进行归的子句，在其间进行归结。就是说，至少有一个子句来自结。就是说，至少有一个子句来自于支撑集于支撑集T T或由或由T T导出的归结式。导出的归结式。3.3谓词逻辑归结原理谓词逻辑归结原理例例如如：A1A2A3A1A2A3B B中中的的B B可可以以作作为为支支撑撑集集运运用用。要要求求每每一一次次参参与与归归结结的的亲亲本本子子句句中中，只只要要应应当当有有一一个个是是有有目目标标公公式式的的否否定定（B B）所所得得到到的的子子句句或或者者它它们们的的后后裔。裔。支支撑撑集集策策略略的的归归结结是是完完备备的的，同同样样，全全部部可可归归结结的的谓谓词词公公式式都都可可以以用用接接受受支支撑撑集集策策略略达达到到加加快快归归结结速速度度的的目目的的。问问题题是是如如何何找找寻寻合合适适的的支支撑撑集集。一一个个最最简简洁洁找找到到的的支支撑撑集是目标子句的非，即集是目标子句的非，即S SB B。3.3谓词逻辑归结原理谓词逻辑归结原理ST可满足支撑集示意图3.3谓词逻辑归结原理谓词逻辑归结原理 语义归结 完备 语义归结策略是将子句S依据确定的语义分成两部分，约定每部分内的子句间不允许作归结。同时还引入了文字次序，约定归结时其中的一个子句的被归结文字只能是该子句中“最大”的文字。语义归结策略的归结是完备的，同样，全部可归结的谓词公式都可以用接受语义归结策略达到加快归结速度的目的。问题是如何找寻合适的语义分类方法，并依据其含义将子句集两个部分中的子句进行排序。3.3谓词逻辑归结原理谓词逻辑归结原理线性归结 完备 线性归结策略首先从子句集中选取一个称作顶子句的子句C0起先作归结。归结过程中所得到的归结式Ci马上同另一子句Bi进行归结得归结式Ci+1。而Bi属于S或是已出现的归结式Cj(j 完备 单元归结策略要求在归结过程中，每次归结都有一个子句是单元子句（只含一个文字的子句）或单元因子。自不待言，词中方法可以简洁地削去另一个非单子句中的一个因子，使其长度削减，构成简洁化，归结效率较高。初始子句集中没有单元子句时，单元归结策略无效。所以说“反之不成立”，即此问题不能接受单元归结策略。3.3谓词逻辑归结原理谓词逻辑归结原理输入归结=完备 与单元归结策略相像，输入归结策略要求在归结过程中，每一次归结的两个子句中必需有一个是S的原始子句。这样可以避开归结出的不必要的新子句加入归结，造成恶性循环。可以削减不必要的归结次数。3.3谓词逻辑归结原理谓词逻辑归结原理犹如单元归结策略，不是全部的可归结谓犹如单元归结策略，不是全部的可归结谓词公式的最终结论都是可以从原始子句集词公式的最终结论都是可以从原始子句集中的得到的。简洁的例子，归结结束时，中的得到的。简洁的例子，归结结束时，即最终一个归结式为空子句的条件是，参即最终一个归结式为空子句的条件是，参与归结的双方必需是两个单元子句。原始与归结的双方必需是两个单元子句。原始子句集中没有单元子句的谓词公式确定不子句集中没有单元子句的谓词公式确定不能接受输入归结策略。能接受输入归结策略。3.3谓词逻辑归结原理谓词逻辑归结原理