三章人工智能蔡自兴

第三章归结推理方法概述命题逻辑的归结法谓词归结子句形归结原理归结过程的策略控制Herbrand定理1归结推理命题逻辑谓词逻辑Skolem标准形、子句集基本概念谓词逻辑归结原理合一和置换、控制策略数理逻辑命题逻辑归结Herbrand定理2第三章归归结推推理方法法概述命题逻辑辑的归结结法谓词归结结子句形形归结原理理归结过程程的策略略控制3概述归结原理理由J.A.Robinson由1965年年提出。。是一阶逻逻辑中至至今为止止的最有有效的半半可判定定的算法法。即，，一阶逻逻辑中任任意恒真真公式，，使用归归结原理理，总可可以在有有限步内内给以判判定。语义网络络、框架架表示、、产生式式规则等等等都是是以推理理方法为为前提的的。即：：有了规规则已知知条件，，顺藤摸摸瓜找到到结果。。而归归结方法法是自动动推理、、自动推推导证明明用的。。（“数数学定理理机器证证明”））本课程只只讨论一一阶谓词词逻辑描描述下的的归结推推理方法法，不涉涉及高阶阶谓词逻逻辑问题题。4第三章归归结推推理方法法概述命题逻辑辑的归结结法谓词归结结子句形形归结原理理归结过程程的策略略控制Herbrand定理理5命题逻辑辑的归结结法命题逻辑辑基础：：定义：合取式：：p与q，记做pΛq析取式：：p或q，记做p∨q蕴含式：：如果果p则q，记做p→q等价式：：p当且仅当当q，记做p<=>q。。。。。。。6命题逻辑辑基础定义：若A无成成假赋值值，则称称A为重言式或或永真式式；若A无成成真赋值值，则称称A为矛盾式或或永假式式；若A至少少有一个个成真赋赋值，则则称A为可满满足的；析取范式式：仅由有有限个简简单合取取式组成成的析取取式。合取范式式：仅由有有限个简简单析取取式组成成的合取取式。7命题逻辑辑基础基本等值值式交换率：p∨q<=>q∨p；pΛq<=>qΛp结合率：(p∨q)∨r<=>p∨(q∨r);(pΛq)Λr<=>pΛ(qΛr)分配率：p∨(qΛr)<=>((p∨q)Λ(p∨r)；pΛ(q∨r)<=>((pΛq)∨(pΛr)8命题逻辑辑基础基本等值值式摩根率:～(p∨q)<=>～pΛ～q；～(pΛq)<=>～p∨～q吸收率:p∨(pΛq)<=>p；pΛ(p∨q)<=>p同一律:p∨0<=>p；pΛ1<=>p蕴含等值值式:p→q<=>～p∨q假言易位位式:p→q<=>～q→～p9命题举例例命题：能能判断真真假（不不是既真真又假））的陈述述句。简单陈述述句描述述事实、、事物的的状态、、关系等等性质。。例如：1．1+1==22．雪是黑色色的。3．北京是中中国的首首都。4．到冥王星星去渡假假。判断一个个句子是是否是命命题，有有先要看看它是否否是陈述述句，而而后看它它的真值值是否唯唯一。以以上的例例子都是是陈述句句，第4句的真真值现在在是假，，随着人人类科学学的发展展，有可可能变成成真，但但不管怎怎样，真真值是唯唯一的。。因此，，以上4个例子子都是命命题。而例如：：1．快点走吧吧！2．到那去？？3．x+y>>10等等句子子，都不不是命题题。10命题表示示公式（（1）将陈述句句转化成成命题公公式。如：设““下雨””为p，“骑车车上班””为q，，1．“只只要不下下雨，我我骑自行行车上班班”。～～p是q的充分条条件，因而，可可得命题题公式：：～p→q2．“只只有不下下雨，我我才骑自自行车上上班”。。～p是q的必要条条件，因而，可可得命题题公式：：q→～p11命题表示示公式（（2）例如：1．“如果我我进城我我就去看看你，除除非我很很累。””设：p，我进城城；q，去看你你；r，我很累累。则则有命题题公式：：～r→(p→q)。2．“应届届高中生生，得过过数学或或物理竞竞赛的一一等奖奖，保送上北北京大学学。”设：p，应届高中中生，q，保送上北北京大学学上学，，r，是得过数数学一等等奖。t，是得过物物理一等等奖。则有命题题公式公公式：p∧(r∨t)→q。12命题逻逻辑的推推理规则则附加：A=>（A∨B)简化：(AΛB)==>A假言推理理:(((A→B)ΛA)==>B拒取式：：((A→B)Λ～B)==>～A析取三段段论：((A∨B)Λ～A)==>B假言三段论：：((A→B)Λ(B→C))=>>(A→C)等价三段段论：((A<—>B)Λ(B<—>C))=>>(A<—>C)构造性两两难：((A→B)Λ(C→D)Λ（A∨C))==>(B∨D)13利用规则则构造证证明例：前提：p∨q,p→～r,s→t,～s→r,～t结论：q证明：①s→t前提引入入②～t前提引入入③～s①②拒取规则则④～s→r前提引入入⑤r③④⑥p→～r前提引入入⑦～p⑤⑥拒取规则则⑧p∨q前提引入入⑨q⑦⑦⑧⑧析取三段段论14命题逻辑辑的归结结法基本单元元：简单命命题（陈陈述句））例：

命题：A1、A2、A3和B求证：A1ΛA2ΛA3成立，则B成立，即：A1ΛA2ΛA3→B反证法：证明A1ΛA2ΛA3Λ～B是矛盾式式（永假式式）15归谬法证证明例：前提：p→（～（rΛs)→q),,p,～s结论：q证明：①p→（～（rΛs)→q)前提引入入②p前提引入入③～（rΛs)→q①②假言推理理④～q否定结论论引入⑤（rΛs)③④拒取式⑥～s前提引入入⑦s⑤简化⑧sΛ～s⑦⑥合取得到矛盾盾结果16命题逻辑辑的归结结法归结原理理是在谓谓词公式式的子句句集合之之上进行行归结的的，因而而首先讨讨论子句句集。建立子句句集合取范式式：命题、、命题和和的与，，如：：PΛ（P∨Q）Λ（～P∨Q）子句集S：合取范式式形式下下的子命命题（元元素）的的集合例：命题题公式：：PΛ（P∨Q）Λ（～P∨Q）子句集S：S={{P,,P∨∨Q,～P∨Q}}17命题逻辑辑的归结结法归结式消除互补补对，求求新子句句→得到归结结式。如子句：：C1,C2，归结式：：R(C1,C2)=C1ΛC2

注意：C1ΛC2→R((C1,C2)，反之不一定成立。18命题逻辑辑的归结结法归结过程程将命题写写成合取取范式求出子句句集对子句集集使用归归结推理理规则归结式作作为新子子句参加加归结归结式为为空子句句□，S是不不可满足足的（矛矛盾），，原命题题成立。。（证明完完毕）谓词的归归结：除了有有量词和和函数以以外，其其余和命命题归结结过程一一样。19命题逻辑辑归结例例题（1）例题，证证明公式式：(P→Q)→→((～Q→→～～P)证明：（1）根根据归结结原理，，将待证证明公式式转化成成待归结结命题公公式：(P→→Q))∧～～(～Q→～～P))（2）分分别将公公式前项项化为合合取范式式：P→Q＝＝～P∨Q结论求～～后的后后项化为为合取范范式：～(～Q→～～P))＝～～(Q∨∨～P))＝～～Q∧∧P两项合并并后化为为合取范范式：（～P∨∨Q）∧～～Q∧∧P（3）则则子句集集为：{～P∨Q，，～Q，，P}20命题逻辑辑归结例例题（2）子句集为为：{{～P∨Q，，～Q，，P}（4）对对子句集集中的子子句进行行归结可可得：1.～～P∨Q2.～～Q3.P4.Q，，（（1，3归归结）5.，（（2，4归归结）由上可得得原公式式成立。。21第三章归归结推推理方法法概述命题逻辑辑的归结结法谓词归结结子句形形归结原理理归结过程程的策略略控制Herbrand定理理22谓词归结结原理基基础一阶逻辑辑基本概念念个体词：：表示主主语的词词谓词：刻刻画个体体性质或或个体之之间关系系的词量词：表表示数量量的词23谓词归结结原理基基础小王是个个工程师师。8是个自自然数。。我去买花花。小丽和小小华是朋朋友。其中，““小王””、“工工程师””、“我我”、““花”、、“8””、“小小丽”、、“小华华”都是是个体词词，而““是个工工程师””、“是是个自然然数”、、“去买买”、““是朋友友”都是是谓词。。显然前前两个谓谓词表示示的是事事物的性性质，第第三个谓谓词“去去买”表表示的一一个动作作也表示示了主、、宾两个个个体词词的关系系，最后后一个谓谓词“是是朋友””表示两两个个体体词之间间的关系系。24谓词归结结原理基基础一阶逻辑辑公式及其其解释个体常量量：a,b,,c个体变量量：x,y,,z谓词符号号：P,Q,,R量词符号号：,25谓词归结结原理基基础例如：（（1）所所有的人人都是要要死的。。（2）有的人活活到一百百岁以上上。在个体域域D为人类集集合时，，可符号号化为：（1）xP(x)，其中P(x)表示x是要死的的。（2）xQ(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活到一百百岁以上上。26谓词归结结原理基基础量词否定定等值式式：～(x）M（x）<=>（y）～M（y）～(x）M（x）<=>（y）～M（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）27谓词归结结原理基基础量词辖域域收缩与与扩张等等值式：(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）28谓词归结结子句形形(Skolem标准形)SKOLEM标准形前束范式式定义：说公式式A是一个前前束范式式，如果果A中的一切切量词都都位于该该公式的的最左边边（不含含否定词词），且且这些量量词的辖辖域都延延伸到公公式的末末端。29谓词归结结子句形形(Skolem标准形)即：把把所有的的量词都都提到前前面去，，然后消消掉所有有量词(Q1x1)(Q2x2)…(Qnxn)M(x1,x2,…,xn)约束变项项换名规规则：(Qx）M（x）<=>（Qy）M（y）(Qx）M（x,z）<=>（Qy）M（y,z）30谓词归结结子句形形(Skolem标准形)量词消去去原则：消去存在在量词““”，即将该量量词约束束的变量量用任意意常量（（a,b）或任意意变量函函数(f(x)、g(y)）代替。。略去任意意量词““”。31谓词归结结子句形形(Skolem标准形)SKOLEM定理：谓词逻辑辑的任意意公式都都可以化化为与之之等价的的前束范范式，但但其前束束范式不不唯一。。SKOLEM标准形定定义：消去量词词后的谓谓词公式式。注意：谓词公公式G的SKOLEM标准形同G并不等值值。32谓词归结结子句形形(Skolem标准形)例:将下式化化为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))由此得到到前述范范式33谓词归结结子句形形(Skolem标准形)第五步，，消去““”（存在在量词）），略去去“”任意量量词消去(y)，因为它左左边只有有(x)，所以使用用x的函数f(x))代替之，，这样得得到：(x)(z)(P(a,x,f(x)))∧～Q(z,,b))∧～R(x)))消去(z)，同理使用用g(x))代替之，，这样得得到：(x)((P((a,x,f(x))∧～Q(g((x),,b))∧～R(x)))则，略去去全称变变量，原原式的Skolem标准形为为：P(a,,x,,f((x)))∧～Q(g((x),,b))∧～R(x))34谓词归结结子句形形子句与子子句集文字：不含任任何连接接词的谓谓词公式式。子句：一些文文字的析析取（谓谓词的和和）。子句集S的求取：G→SKOLEM标准形→消去存在在变量→以“，”取代“Λ”，并表示为为集合形形式。。35谓词归结结子句形形G是不可可满足的的<=>S是不可可满足的的G与S不等价，，但在不不可满足足的意义义下是一一致的。。定理：若G是给给定的公公式，而而S是相相应的子子句集，，则G是是不可满满足的<=>S是不可可满足的的。

注意：G真不一一定S真真，而S真必有有G真。。即：S=>G36谓词归结结子句形形G=G1ΛG2ΛG3Λ…ΛΛGn的子句形形G的字句集集可以分分解成几几个单独独处理。。

有SG=S1US2US3U…USn则SG与S1US2US3U…USn在不可满满足得意意义上是是一致的的。即SG不可满足足<=>S1US2US3U…USn不可满足足37求取子句句集例((1)例：对所所有的x,y,,z来说说，如果果y是x的父亲亲，z又又是y的的父亲，，则z是是x的祖祖父。又又知每个个人都有有父亲，，试问对对某个人人来说谁谁是他的的祖父？？求：用一一阶逻辑辑表示这这个问题题，并建建立子句句集。解：这里里我们首首先引入入谓词：：P(x,,y))表示示x是y的父亲亲Q(x,,y))表示示x是y的祖父父ANS((x)表表示问问题的解解答38求取子句句集例((2)对于第一一个条件件，“如果果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)S～B：～Q((x,y)∨ANS((x)则得到的的相应的的子句集集为：{{SA1，SA2，S～B}39第三章归归结推推理方法法概述命题逻辑辑的归结结法谓词归结结子句形形归结原理理归结过程程的策略略控制Herbrand定理理40归结原理理归结原理理正确性性的根本本在于，，找到矛矛盾可以以肯定不不真。方法：和命题逻逻辑一样样。但由于有有函数，，所以要要考虑合一和置换。41置换置换：可以简简单的理理解为是是在一个个谓词公公式中用用置换项项去置换换变量。。定义：置换是形形如{t1/x1,t2/x2,…,,tn/xn}的有限限集合。。其中，，x1,x2,…,,xn是互不相相同的变变量，t1,t2,…,,tn是不同于于xi的项（常量、变变量、函函数）；ti/xi表示用ti置换xi，并且要要求ti与xi不能相同同，而且且xi不能循环环地出现现在另一一个ti中。在谓词逻逻辑的归归结过程程中，寻寻找项之之间合适适的变量量置换使使表达式式一致是是一个很很重要的的过程，，这个过过程称为为合一。42例{a/x，c//y，f(b))/z}}是一个个置换{g(y)/x，f((x)//y}不不是一个个置换。。原因：它在x和y之之间出现现了循环环置换现现象。置置换的目目的是要要将某些些变量用用另外的的变量、、常量或或函数取取代，使使其不在在公式中中出现。。这里用用g(y)置换换x,用用f((g(y))置置换y,,既没有有消去x,也没没有消去去y.若若改为为{g(a)/x，f((x)//y}就可以了了。43置换的合合成设＝{t1/x1,t2/x2,…,,tn/xn}，＝{u1/y1,u2/y2,…,,un/yn}，是两两个置换换。则与的合成也也是一个个置换，，记作·。它是从从集合{t1·/x1,t2·/x2,…,,tn·/xn,u1/y1,u2/y2,…,,un/yn}中删去以以下两种种元素：：当ti=xi时，删去去ti/xi(i==1,,2,,…,,n));当yi{x1,x2,…,,xn}时，删删去uj/yj(j==1,,2,,…,,m))最后剩下下的元素素所构成成的集合合。合成即是是对ti先做置换然后后再做置换，置置换xi44置换的合合成例：设：＝{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}}＝{t1//x1,,t2/x2,……,tn/xn}，＝{u1//y1,,u2/y2,……,un/yn}，·={t1··/x1,,t2·/x2,,…,,tn·/xn,u1/y1,u2/y2,……,un//yn}当ti=xi时，删去去ti/xi((i==1,2,……,n);当yi{x1,,x2,,…,,xn}时，删去去uj/yj(j==1,,2,,…,,m))45合一合一可以简单单地理解解为“寻寻找相对对变量的的置换，，使两个个谓词公公式一致致”。定义：设有公公式集F＝{F1，F2，…，Fn}，若存存在一个个置换，可使F1＝F2＝…=Fn，则称是F的一一个合一一。同时时称F1，F2，....，Fn是可合一一的。

例：设有公式式集F＝＝{P((x,y,f(y)),,P((a,g(x)),z))}，则则＝{a//x,g(a)/y,f(g((a)))/z}}是它的的一个合合一。注意：一一般说来来，一个个公式集集的合一一不是唯唯一的。。46例1：设有置换换s={z/x,A//y}，则：P[x,f(y),B]s=P[z,f(A),B]。这里x被换成了了z，y被换成了了A。设有公式式的集合合{Ei}((i=1,2,.....,m)，如果存存在一个个置换s，使得这这m个公式被被施以s以后，变变得完全全一样了了，则称称这m个公式是是可合一一的，置置换s是它们的的合一者者。47例2：设有公式式集{P(x,f(y),B),P(z,f(B),B)}和置换s1={{A/x,B/y,,A//z}，由于：：P(x,f(y),B)s=P(A,f(B),B)P(z,f(B),B)s=P(A,f(B),B)所以公式式集{P(x,f(y),B),P(z,f(B),B)}是可合一一的，置置换s1={{A/x,B/y,,A//z}是它们的的合一者者。48若存在一一个置换换s使得得表达式式集{Ei}中中每个元元素经置置换后的的例有：：E1s=E2s=E3s==…，，则称表表达式集集{Ei}是可可合一的的，这个个置换s称作{{Ei}}的合一一者。在归结法法中主要要是处理理可合一一的子句句集，例例如有子子句集::{P（x，f（（y），，B），，P（x，f（（B），，B）}}，若对对两个子子句作置置换s＝＝{A//x，B/y}}，则可可得{P（A，，f（B），B）}，，因而该该子句集集是可合合一的。。仅仅从合合一的角角度看，，s并不不是最简简单的合合一者，，因为还还存在另另一个s1＝{{B/y}的合合一者，，使子句句集合一一为{P[x，，f（B），B]}。。因此通通常还要要求找的的是最一一般或最最普通的的合一者者（mostgeneralunifier）g，，记为mgug。49任一合一一者s与与g之间间的关系系是：存在一个个置换s′，使使得{Ei}s＝{Ei}gs′。。再比较较上例的的两个合合一者，，有{A/x，，B/y}＝{{B/y}{A/x}}，因此此mgug＝＝{B//y}。。可见mgug的置置换限制制最少，，所产生生的例更更一般化化，这有有利于归归结过程程的灵活活使用。。50UNIFY算法法UNIFY算法法不仅可可以判断断两个公公式是否否可合一一，而且且在可合合一的情情况下，，给出它它们的mgu。。该算法法为了表表述上的的方便，，假定谓谓词是以以表的形形式表示示的。如谓词P(x,,f((y),,B))表示为为(Px((fy)B)。UNIFY算法法的基本本思想是是，从左左向右按按位置扫扫描两个个谓词的的每一个个对应部部分，如如果二者者一致，，则转入入下一项项。如果果不一致致，则看看是否存存在一个个置换，，使得对对应项经经过置换换后是一一致的。。如果不不存在这这样的置置换，则则两个公公式是不不可合一一的。如如果两个个谓词的的对应部部分都是是一致的的，或者者经置换换后是一一致的，，则两个个公式是是可合一一的，这这些置换换的合成成是它们们的合一一者。如如果当两两个对应应项都是是变量时时，置换换选作用用一个变变量代替替另一个个变量，，则这样样得到的的合一者者是mgu。51例：公公式集如如下：{{P((x,x,z),,P((f(y),f(B),y)}}

用表表的形式式表示为为：E1=((Pxxz))

E2=(P(fy))(fB))y)从左向右右按顺序序扫描两两个谓词词。E1和E2的第一一项都是是P，是是一致的的，转入入第二项项。E1的第二二项是x，E2的第二二项是((fy)，二二者不一一致。由由于其中中一个是是变量，，可以进进行置换换。选置置换{((fy)/x}使得得二者成成为一致致的。该该置换同同时作用用于E1的第三三项x。。这样有有：E1=((P((fy)((fy)z))

E2=((P((fy)((fB)B)52E1=((P((fy))(fy))z)E2=((P((fy)((fB)B)继继续看看第三项项。E1的第三三项是((fy)，E2的第第三项是是(f,,B))。由于于两个都都是表，，需要进进入表的的内部进进行比较较。在表的内内部，第第一项均均是f，，是一致致的。第第二项一一个是变变量y，，一个是是常量B。选置置换{B/y}}使二者者成为一一致的。。该置换换不仅使使得两个个公式中中的所有有y都被被替换为为了B，，而且也也作用于于前一个个置换{{(fy)//x}，，使得该该置换变变成了{{(fB)//x}。。这样有有：E1=((P((fB)((fB)z))

E2=((P((fB)((fB)B)53E1=((P((fB)((fB)z))

E2=((P((fB)((fB)B)E1的第第四项是是变量z，E2的第四四项是常常量B，，选置换换{B//z}使使得二者者成为一一致的。。有：E1==(P(fB))(fB))B))

E2=((P((fB)((fB)B)至至此，E1和E2是完完全一样样的了，，说明E1和E2是可可合一的的。其合合一者是是这一过过程中几几个置换换的并{{(fB)//x,B/y,B/z}}，该合合一者也也是mgu。54如果这一一过程中中有某一一个对应应项是不不能置换换为一样样的，则则说明两两个公式式不可合合一。如如该例如如果是：：

E1=(PxxA))

E2=(P(fy))(fB))y)则则是不可可合一的的。因为为经过几几步变换换后有：：

E1=((P((fB)((fB)A)E2=((P((fB)((fB)B)此此时E1的第第四项是是常量A，而E2的第第四项是是常量B，二者者不一致致，而且且都是常常量，无无法置换换。因此此两个公公式不可可合一。。55P105例例3.16W={P(a,,x,f(g((y)))),P(z,,f(a),f(u))},其其中F1=P(a,,x,f(g((y)))),F2==P(z,f((a),,f(u),求求F1和F2的mgu56谓词逻辑辑的归结结过程对于谓词词逻辑来来说，可可以这样样判断两两个子句句是否可可进行归归结，及及其归结结式是什什么。对于子句句C1''∨L1和C2'∨L2，如如果L1与～L2可合合一，且且s是其其合一者者，则((C1''∨C2')s是其归归结式。。其中L1、L2是单单文字。。事实上上L1、、L2中中有一个个含有否否定符，，所以对对另一个个加上否否定符后后，才能能判断它它们是否否可合一一。57设C1和和C2为为两个不不同的子子句，子子句中的的变量已已标准化化。我们们采用文文字集的的形式来来表示子子句（即即文字之之间理解解为析取取关系）），则有有C1＝{C1i}}（i＝＝1，2，…，，n），，C2＝{{C2j}（j＝1，，2，……，m））

再设设{L1k}和和{L2k}分分别为C1和C2的两两个子集集。若若{L1k}和和{~L2k}}的并集集存在一一个mgus，则两两个子句句的归结结式为C＝{{{C1i}－{{L1k}}s∪{{{C2j}－{{L2k}}s

可以以看出对对这两个个子句进进行归结结时，由由于有多多种方式式选取{{L1k}和{{L2k}，因因此归结结式不是是唯一的的。58例：C1＝P（x，，f（A））∨∨P（x，f（（y）））∨Q（（y）C2＝＝~P（（z，f（A）））∨~~Q（z）①①取L11＝＝P（x，f（（A））），L21＝~~P（z，f（（A）））存在s＝{z/x}},使L11和和~L21合一一，所以以归结式式为P（z，，f（y））∨∨Q（y）∨~~Q（z）②取L11＝＝P（x，f（（y））），L21＝~~P（z，f（（A）））则则s＝（z/x，，A/y），归结式为为Q（A））∨~Q（z））③取L11＝＝Q（y），L21＝＝~Q（（z）则则s＝{y/z}}，归结式式为P（x，，f（A））∨∨P（x，f（（y）））∨~P（y，，f（A））

59这个例子子说明，，选择不不同文字字对做归归结时可可得到不不同的归归结式，，但由于于都是用用最一般般的合一一者作置置换，因因此这些些归结式式仍是最最一般的的归结式式。就是是说，如如果对某某个文字字不是用用mgu来合一一，那么么得到的的归结式式比最一一般的归归结式则则有较多多的限制制。实际际上我们们总是希希望用最最一般的的归结式式，以增增加归结结过程的的灵活性性。60归结原理理归结的注意事项项：谓词的一一致性，名称不不一致的的谓词，，如P()与Q()，不可以常量的一一致性，含有不不同常量量的谓词词，如P(a,…))与P(b,,….))，不可以如果是常常量与变变量，P(a,,…..)与P(x,,…))，可以3.变量与函函数，P(x,x,,…..)与P(x,,f((x),,…))，不可以,因为不能能进行{x/f((x)}的置换；；但P(x,x,,…..)与P(x,f(y),……)，可以通通过对两两式分别别做{f(y))/x}置换，而而后进行行归结。。4.不能同时时消去两两个互补补对，P∨Q与～P∨～Q的空，不不可以5.先进行内内部简化化，再进进行置换换与合并并。61例：设C1=P(y))∨P((f(x))∨∨Q(g(x)),C2=～P(f((g(a))))∨Q((b),求C1和C2的归结式式。解：对C1,取最一般般合一={f(x))/y}得C1的因子C1=P(f((x))∨Q(g((x))C1与C2归结，2={f(x))/y,,g(a)/x}得归结式式：Q(g((g(a))))∨Q((b)62归结原理理归结的过过程写出谓词词关系公公式→用反演法法写出谓谓词表达达式→SKOLEM标准形→子句集S→对S中可归结结的子句句做归结结→归结式仍仍放入S中，反复复归结过过程→得到空子子句▯得证63例题“快乐学学生”问问题假设任何何通过计计算机考考试并获获奖的人人都是快快乐的，，任何肯肯学习或或幸运的的人都可可以通过过所有的的考试，，张不肯肯学习但但他是幸幸运的，，任何幸幸运的人人都能获获奖。求求证：张张是快乐乐的。64例题“快乐学学生”问问题解：先将将问题用用谓词表表示如下下：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)65例题“快乐学学生”问问题由R1及及逻辑转转换公式式:P∧W→H==～～（P∧∧W）∨∨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))66归结原理理归结法的的实质归结法是是仅有一一条推理理规则的的推理方方法。归结的过过程是一一个语义义树倒塌塌的过程程。归结法的的问题子句中有有等号或或不等号号时，完完备性不不成立。。※Herbrand定理的不不实用性性引出了了可实用用的归结结法。67第三章归归结推推理方法法概述命题逻辑辑的归结结法谓词归结结子句形形归结原理理归结过程程的策略略控制Herbrand定理理68归结过程程的控制制策略要解决的的问题：归结方法法的知识识爆炸。。控制策略略的目的的归结点尽尽量少控制策略略的原则则给出控制制策略，，以使仅仅对选择择合适的的子句间间方可做做归结。。避免多多余的、、不必要要的归结结式出现现。或者者说，少少做些归归结仍能能导出空空子句。。69控制策略略的方法法(1)删除策略略=>完备名词解释释：归类类：设有有两个子子句C和D，若有置换换使得CD成立，则则称子句句C把子句D归类。由于小的的可以代代表大的的，所以以小的吃吃掉大的的了。若对S使用归结结推理过过程中，，当归结结式Cj是重言式式（永真真式）和和Cj被S中子句和和子句集集的归结结式Ci(i<j)所归类时时，便将将Cj删除。这这样的推推理过程程便称做做使用了了删除策策略的归归结过程程。主要思想想：归结过过程在寻寻找可归归结子句句时，子子句集中中的子句句越多，，需要付付出的代代价就会会越大。。如果在在归结时时能把子子句集中中无用的的子句删删除掉，，就会缩缩小搜索索范围，，减少比比较次数数，从而而提高归归结效率率。删除除策略对对阻止不不必要的的归结式式的产生生来缩短短归结过过程是有有效的。。然而要要在归结结式Cj产生后方方能判别别它是否否可被删删除，这这部分计计算量是是要花费费的，只只是节省省了被删删除的子子句又生生成的归归结式。。尽管使使用删除除策略的的归结，，少做了了归结但但不影响响产生空空子句，，就是说说删除策策略的归归结推理理是完备备的。70控制策略略的方法法(2)采用支撑撑集<=>完备支撑集：设有不不可满足足子句集集S的子集T，如果S-T是可满足足的，则则T是支持集集。采用支撑撑集策略略时，从从开始到到得到的整个归归结过程程中，只只选取不不同时属属于S-T的子句，，在其间间进行归归结。就就是说，，至少有有一个子子句来自自于支撑撑集T或由T导出的归归结式。。例如：A1ΛA2ΛA3Λ～B中的～B可以作为为支撑集集使用。。要求每每一次参参加归结结的亲本本子句中中，只要要应该有有一个是是有目标标公式的的否定（（～B）所得到的的子句或或者它们们的后裔裔。支撑集策策略的归归结是完完备的，，同样，，所有可可归结的的谓词公公式都可可以用采采用支撑撑集策略略达到加加快归结结速度的的目的。。问题是是如何寻寻找合适适的支撑撑集。一一个最容容易找到到的支撑撑集是目目标子句句的非，，即S～B。71ST可满足支撑集示意图72控制策略略的方法法(3)语义归结结<=>完备语义归结结策略是将子句句S按照一定定的语义义分成两两部分，，约定每每部分内内的子句句间不允允许作归归结。同同时还引引入了文文字次序序，约定定归结时时其中的的一个子子句的被被归结文文字只能能是该子子句中““最大””的文字字。语义归结结策略的的归结是是完备的的，同样样，所有有可归结结的谓词词公式都都可以用用采用语语义归结结策略达达到加快快归结速速度的目目的。问问题是如如何寻找找合适的的语义分分类方法法，并根根据其含含义将子子句集两两个部分分中的子子句进行行排序。。73控制策略略的方法法(4)线性归结结<=>完备线性归结结策略首先从子子句集中中选取一一个称作作顶子句句的子句句C0开始作归归结。归归结过程程中所得得到的归归结式Ci立即同另另一子句句Bi进行归结结得归结结式Ci+1。而Bi属于S或是已出出现的归归结式Cj(j<i)。即，如下下图所示示归结得得到的新新子句立立即参加加归结。。线性归结结是完备备的，同同样，所所有可归归结的谓谓词公式式都可以以采用线线性归结结策略达达到加快快归结速速度的目目的。如如果能搞搞找到一一个较好好的顶子子句，可可以式归归结顺利利进行。。否则也也可能事事与愿违违。74C0C1C2C3C4C5空线性归结策略示意图75控制策略略的方法法(5)单元归结结=>完备单元归结结策略要求在归归结过程程中，每每次归结结都有一一个子句句是单元元子句（（只含一一个文字字的子句句）或单单元因子子。显而而易见，，词中方方法可以以简单地地削去另另一个非非单子句句中的一一个因子子，使其其长度减减少，构构成简单单化，归归结效率率较高。。初始子句句集中没没有单元元子句时时，单元元归结策策略无效效。所以以说“反反之不成成立”，，即此问问题不能能采用单单元归结结策略。。76控制策略略的方法法(6)输入归结结=>完备与单元归归结策略略相似，，输入归归结策略略要求在在归结过过程中，，每一次次归结的的两个子子句中必必须有一一个是S的原始子子句。这这样可以以避免归归结出的的不必要要的新子子句加入入归结，，造成恶恶性循环环。可以以减少不不必要的的归结次次数。如同单元元归结策策略，不不是所有有的可归归结谓词词公式的的最后结结论都是是可以从从原始子子句集中中得到的的。简单单的例子子，归结结结束时时，即最最后一个个归结式式为空子子句的条条件是，，参加归归结的双双方必须须是两个个单元子子句。原原始子句句集中没没有单元元子句的的谓词公公式一定定不能采采用输入入归结策策略。77第三章归归结推推理方法法概述命题逻辑辑的归结结法谓词归结结子句形形归结原理理归结过程程的策略略控制Herbrand定理理78Herbrand定理问题：一阶逻辑辑公式的的永真性性（永假假性）的的判定是是否能在在有限步步内完成成？79Herbrand定理1936年图灵(Turing)和邱吉(Church)互相独立立地证明明了：“没有一一般的方方法使得得在有限限步内判判定一阶阶逻辑的的公式是是否是永永真（或或永假））。但是是如果公公式本身身是永真真（或永永假）的的，那么么就能在在有限步步内判定定它是永永真（或或永假））。对于于非永真真（或永永假）的的公式就就不一定定能在有有限步内内得到结结论。判判定的过过程将可可能是不不停止的的。”80Herbrand定理Herbrand的思思想定义：公式G永永真：对于G的所有有解释，，G都为为真。思想：寻找一个个已给的的公式是是真的解解释。然然而，如如果所给给定的公公式的确确是永假假的，就就没有这这样的解解释存在在，并且且算法在在有限步步内停止止。81Herbrand定理H域H解释语义树结论：Herbrand定理理82Herbrand定理理（H域）基本方法法：因为量词是任任意的，，所讨论论的个体体变量域域D是任意的的，所以以解释的的个数是是无限、、不可数数的。简化讨论论域。建立一一个比较较简单、、特殊的的域，使使得只要要在这个个论域上上，该公公式是不可满足足的。此域称为为H域。83D域H域H域与D域关系示意图84H域例题设子句集集S={{P(x)),Q(y,,f(z,b))),R(a))}，求H域解：H0＝{a,b}为子句集集中出现现的常量量H1＝{a,b,f(a,b)),f(a,,a),,f((b,a),f(b,b))}H2＝{a,,b,,f((a,b),f(a,a)),f(b,,a),,f((b,b)，f(a,,f(a,b))),f(a,f((a,a)),,f((a,f(b,a))),f(a,f(b,,b))),f(b,,f(a,b))),f(b,f((a,a)),,f((b,f(b,a))),f(b,f((b,b)),,f(f((a,b),f(a,,b))),f(f((a,b),f(a,,a))),f(f((a,b),f(b,a))),f(f(a,,b),,f((b,b)),,f(f((a,a),f(a,,b))),f(f((a,a),f(a,,a))),f(f((a,a),f(b,a))),f(f(a,,a),,f((b,b)),,f(f((b,a),f(a,,b))),f(f((b,a),f(a,,a))),f(f((b,a),f(b,a))),f(f(b,,a),,f((b,b)),,f(f((b,b),f(a,,b))),f(f((b,b),f(a,,a))),f(f((b,b),f(b,a))),f(f(b,,b),,f((b,b))}}………H∞=H1∪H2∪H3………85Herbrand定理理（H域）几个基本本概念f（tn）：f为子句集集S中的所有有函数变变量。t1,t2,…tn为S的H域的元素素。通过过它们来来讨论永永真性。。原子集A：谓词套上H域的元素素组成的的集合。。如A={{所有形如如P(t1,t2,…tn)的元素}即把H中的东西西填到S的谓词里里去。S中的谓词词是有限限的，H是可数的的，因此此，A也是可数数的。86原子集例例题上例题的的原子集集为：A={{P(a)),Q(a,,a)),R(a)),P(b)),Q(b,,a)),Q(b,,b)),Q(a,b)),R(b)),P(f(a,,b))),Q(f((a,b),,f((a,b))),R(f((a,b),,P(f((a,a)),,P((f(b,a))),P(f((b,b)),,……))一旦原子子集内真真值确定定好（规规定好）），则S在H上的真值值可确定定。成为为可数问问题。87Herbrand定理H域H解释语义树结论：Herbrand定理理88Herbrand定理理（H解释）解释I：谓词公式式G在论域D上任何一一组真值值的指定定称为一一个解释释。H解释：子子句集S在的H域上的解解释称为为H解释。问题：对于所有有的解释释，全是是假才可可判定。。因为所所有解释释代表了了所有的的情况，，如可穷穷举，问问题便可可解决。89Herbrand定理理（H解释）基原子、、基文字字、基子子句、基基子句集集：没有变量量出现的的原子、、文字、、子句和和子句集集，分别别称为基基原子、、基文字字、基子子句、基基子句集集。基例：子句集集S中某子句句C中所有变变元符号号均以S的H域中的元元素代入入后，所所得的基基子句C’称为C的一个基基例。由定义可可知，若若一个解解释I*使得某个个基子句句为假，，则此解解释I*为假。90例:S={{P(x)∨∨Q((X),,R(f(y)))},,求其一一个H解解释I**.解：S的H域域为：{{a,f(a),f(f(a))),……}S的原子子集为：：{P((a),,Q(a),R(a)),P((f(a)),,Q(f(a))),R(f((a))),…}}凡对A中中各元素素真假值值的一个个具体设设定都为为S的一一个H解解释，如如：I1*=={P((a),,Q(a),R(a)),P((f(a)),,Q(f(a))),R(f((a))),…}}I2*=={～P(a),～～Q(a)),～～R((a),,～P(f(a))),Q(f(a))),R(f(a))),……}I3*=={P(a)),～～Q((a),,～R(a),P(f(a))),Q(f(a))),～～R(f((a))