人工智能原理教案章归结推理方法归结推理方法

第二章归结推理方法,课前指导2.1归结原理概述2.2命题逻辑的归结2.3谓词逻辑归结法基础2.4归结原理2.5归结过程控制策略2.6Herbrand定理章节小结,课前指导,【学习目标】本章主要讨论命题逻辑和一元谓词逻辑的归结推理方法。同学需要在熟练掌握一般逻辑知识的基础上，学习Skolem标准形和Herbrand定理，从而对归结原理有一个比较透彻的了解。【学习指南】在学习新知识的同时回顾以前所学的一般逻辑知识。对所涉及的概念和方法不要死记硬背，对于比较抽象的概念，可以通过比较简单的例子来理解。【难重点】应该熟练掌握把逻辑公式的合取范式、Skolem标准形的转化方法、归结法进行归结的过程，掌握线性归结、支撑集归结等归结策略。,【知识点】归结方法的特点、与其它推理方法的比较命题逻辑基础，前束范式，约束变量换名规则Skolem标准形的定义，子句和子句集，定理的内容及推广H域、H解释、语义树合一和置换，归结过程归结法的控制策略的原则及基本方法。,归结推理知识结构,2.1归结原理概述,归结原理由J.A.Robinson于1965年提出，又称为消解原理。该原理是Robinson在Herbrand理论基础上提出的一种基于逻辑的、采用反证法的推理方法。由于其理论上的完备性，归结原理成为机器定理证明的主要方法。注意：本课程只讨论一阶谓词逻辑描述下的归结推理方法，不涉及高阶谓词逻辑问题本章首先介绍命题逻辑的归结，并以此为基础介绍谓词逻辑的归结过程及相关的思想、概念和定义，最后给出谓词逻辑归结的基础Herbrand定理的一般形式。,定理证明的实质与困难,从某种意义上讲大部分人工智能问题都可以转化为一个定理证明问题。定理证明的实质：就是要对给出的（已知的）前提和结论，证明此前提推导出该结论这一事实是永恒的真理。这是非常困难的，几乎是不可实现的。困难所在：要证明在一个论域上一个事件是永真的，就要证明在该域中的每一个点上该事实都成立。很显然，论域是不可数时，该问题不可能解决。即使可数，如果该轮域是无限的，问题也无法简单地解决。Herbrand采用了反证法的思想，将永真性的证明问题转化成为不可满足性的证明问题。Herbrand理论为自动定理证明奠定了理论基础，而Robinson的归结原理使得自动定理证明得以实现。因此，归结推理方法在人工智能推理方法中有着很重要的历史地位。,归结法的特点,与演绎法完全不同，归结法是一种新的逻辑演算算法。它是一阶逻辑中，至今为止的最有效的半可判定的算法。也是最适合计算机进行推理的逻辑演算方法。半可判定，即，一阶逻辑中任意恒真公式，使用归结原理，总可以在有限步内给以判定（证明其为永真式）。,归结法基本原理,归结法的基本原理：是采用反证法或者称为反演推理方法，将待证明的表达式（定理）转换成为逻辑公式（谓词公式），然后再进行归结，归结能够顺利完成，则证明原公式（定理）是正确性的。例如：由命题逻辑描述的命题：A1、A2、A3和B，要求证明：如果A1A2A3成立，则B成立，即：A1A2A3B是重言式（永真式）。归结法的思路：A1A2A3B是重言式等价于A1A2A3B是矛盾式，也就是说永假式。反证法：证明A1A2A3B是矛盾式（永假式）归结的目的：建立基本规则证明该条定理（事实）成立。,归结法和其它推理方法的比较,语义网络、框架表示、产生式规则等知识表示方法的推理都是以逻辑推理方法为前提的。即，有了规则和已知条件，就能够依据一定的规则和公理顺藤摸瓜找到结果。而归结方法是计算机自动推理、自动推导证明用的推理方法。（同样的内容可以在“数学定理机器证明”中找到。）,2.2命题逻辑的归结,2.2.1命题逻辑基础逻辑可分为经典逻辑和非经典逻辑经典逻辑包括命题逻辑和谓词逻辑。归结原理是一种主要基于谓词（逻辑）知识表示的推理方法，而命题逻辑是谓词逻辑的基础。因此，在讨论谓词逻辑之前，先讨论命题逻辑的归结，便于内容上的理解。本节中，将主要介绍命题逻辑的归结方法，以及有关的一些基础知识和重要概念，如数理逻辑基本公式变形、前束范式、子句集等。,命题例子,命题：非真即假的简单陈述句。简单陈述句描述事实、事物的状态、关系等性质。例如：1、1+1=2.2、雪是黑色的。3、北京是中国的首都。4、到冥王星去度假。判断一个句子是否是命题，首先要看它是否是陈述句，而后看它的真值是否唯一。以上的例子都是陈述句，第4句的真值现在是假，随着人类科学的发展，有可能变成真。但不管怎样，真值是唯一的。因此以上例子都是命题。而例如：1、快点走吧！2、到哪去？3、X+Y10等等句子，都不是命题。,命题表示公式（1）,如何将陈述句转化成命题公式？例如：设“下雨”为p，“骑车上班”为q，1、“只要不下雨，我骑自行车上班”。p是q的充分条件，因而，可得命题公式：pq2、“只有不下雨，我才骑自行车上班”。p是q必要条件，因而，可得命题公式：qp,命题表示公式（2）,1、“如果我进城我就去看你，除非我很累。”设：p，我进城；q，去看你；r，我很累。则有命题公式：r(pq)2、“应届高中生，得过数学或物理竞赛的一等奖，保送上北京大学。”设：p，应届高中生；p，保送上北京大学；r，得过数学一等奖；t，得过物理一等奖。则有命题公式：p(rt)q,数理逻辑的基本定义,合取式：p与q，记做pq析取式：p或q，记做pq蕴含式：如果p则q，记做pq等价式：p当且仅当q，记做pq若A无成假赋值，则称A为重言式或永真式；若A无成真赋值，则称A为矛盾式或永假式；若A至少有一个成真赋值，则称A为可满足的；析取范式：仅由有限个简单合取式组成的析取式合取范式：仅由有限个简单析取式组成的合取式,数理逻辑的基本等值式（24个）,交换律：pqqp；pqqp结合律：(pq)rp(qr);(pq)rp(qr)分配律：p(qr)(pq)(pr)；p(qr)(pq)(pr)双重否定律：pp等幂律：ppp；ppp摩根律:(pq)pq；(pq)pq吸收律:p(pq)p；p(pq)p,同一律:p0p；p1p零律：p11p00排中律：pp1矛盾律：pp0蕴含等值式：pqpq等价等值式：pq(pq)(qp)假言易位式:pqpq等价否定等值式：pqpq归谬论：(pq)(pq)p,合取范式,合取范式：单元子句、单元子句的或（）的与（）。如：P（PQ）（PQ）例：求取P(QR)S的合取范式解：P(QR)S=（P(QR)）S=P(QR)S=P(QR)S=P(QR)S=PS(QR)=(PSQ)(PSR)注意：首先一定要将原有的命题公式整理、转换成为各个或语句的与，不然后续推导没有意义。转换是基于数理逻辑的基本等值公式进行的，或转换到与中。思路与代数学的提取公因式方法相似。,子句集,命题公式的子句集S是合取范式形式下的子命题（元素）的集合。子句集是合取范式中各个合取分量的集合，生成子句集的过程可以简单地理解为将命题公式的合取范式中的与符号“”，置换为逗号“，”。上例转换的合取范式：(PSQ)(PSR)其子句集为S=PSQ,PSR又如，有命题公式：P（PQ）（PQ）其子句集S：S=P,PQ,PQ,2.2.2命题逻辑的归结,归结法推理的核心是求两个子句的归结式，因此需要先讨论归结式的定义和性质。归结式的定义设C1和C2是子句集中的任意两个子句，如果C1中的文字L1与C2中的文字L2互补，那么可从C1和C2中分别消去L1和L2，并将C1和C2中余下的部分按析取关系构成一个新子句C12，则称这一个过程为归结，称C12为C1和C2的归结式，称C1和C2为C12的亲本子句。例如：有子句：C1PC1，C2PC2存在互补对P和P，则可得归结式：C12=C1C2注意：C1C2C12，反之不一定成立。,归结式是原两子句的逻辑推论,证明归结式是原两子句的逻辑推论，或者说任一使C1、C2为真的解释I下必有归结式C12也为真。证明：设I是使C1，C2为真的任一解释，若I下的P为真，从而P为假，必有I下C2为真，故C12为真。若不然，在I下P为假，从而I下C1为真，故I下C12为真。于是C1C2为真。于是C1C2R(C1,C2)成立。反之不一定成立，因为存在一个使C1C2为真的解释I，不妨设C1为真，C2为假。若P为真，则PC2就为假了。因此反之不一定成立。由此可得归结式的性质。归结式的性质：归结式C12是亲本子句C12和C12的逻辑结论。,命题逻辑的归结法推理过程,命题逻辑的归结过程也就是推理过程。推理是根据一定的准则由称为前提条件的一些判断导出称为结论的另一些判断的思维过程。命题逻辑的归结方法推理过程：建立待归结命题公式首先根据反证法将所求证的问题转化成为命题公式，求证其是矛盾式（永假式）。求取合取范式建立子句集归结,归结步骤,归结法是在子句集S的基础上通过归结推理规则得到的，归结过程的最基本单元是得到归结式的过程。从子句集S出发，对S的子句间使用归结推理规则，并将所得归结式仍放入到S中（注意：此过程使得子句集不断扩大，是造成计算爆炸的根本原因），进而再对新子句集使用归结推理规则。重复使用这些规则直到得到空子句。这便说明S是不可满足的，从而与S所对应的定理是成立的。归结步骤：1)对子句集中的子句使用归结规则2)归结式作为新子句加入子句集参加归结3)归结式为空子句为止。（证明完毕）得到空子句，表示S是不可满足的（矛盾），故原命题成立。,例题2-1:证明公式：(PQ)(QP)证明:(1)根据归结原理,将待证明公式转化成待归结命题公式：(PQ)(QP)(2)分别将公式前项化为合取范式：PQPQ结论求后的后项化为合取范式：(QP)(QP)QP两项合并后化为合取范式：（PQ）QP(3)则子句集为：PQ，Q，P(4)对子句集中的子句进行归结可得：1.PQ2.Q3.P4.Q（1，3归结）5.（2，4归结）由上可得原公式成立。,2.3谓词逻辑归结法基础,由于谓词逻辑与命题逻辑不同，有量词、变量和函数，所以在生成子句集之前要对逻辑公式做处理，具体的说就是要将其转化为Skolem标准形，然后在子句集的基础上再进行归结，虽然基本的归结的基本方法都相同，但是其过程较之命题公式的归结过程要复杂得多。本节针对谓词逻辑归结法介绍Skolem标准形、子句集等一些必要的概念和定理。,前束范式,前束范式：A是一个前束范式，如果A中的一切量词都位于该公式的最左边（不含否定词），且这些量词的辖域都延伸到公式的末端。前束范式A的形式为：(Q1x1)(Q2x2)(Qnxn)M(x1,x2,xn)即：把所有的量词都提到前面去。注意：由于所有的量词的辖域都延伸到公式的末端，即，最左边量词将约束表达式中的所有同名变量。所以将量词提到公式最前端时存在约束变量换名问题。要严守规则。,约束变量换名规则：(Qx)M（x）（Qy）M（y）(Qx)M（x,z）（Qy）M（y,z）量词否定等值式：(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）量词辖域收缩与扩张等值式：(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）,2.3.1Skolem标准形,Skolem标准形的定义：前束范式中消去所有的存在量词，则称这种形式的谓词公式为Skolem标准形。注意：公式G的SKOLEM标准形同G并不等值。Skolem定理：谓词逻辑的任意公式都可以化为与之等价的前束范式，但其前束范式不唯一。Skolem标准形的转化过程为，依据约束变量换名规则，首先把公式变型为前束范式，然后依照量词消去原则消去或者略去所有量词。,消去量词,量词消去原则：1)消去存在量词“”。即，将该量词约束的变量用任意常量（a,b等）、或全称变量的函数(f(x),g(y)等)代替。如果存在量词左边没有任何全称量词，则只将其改写成为常量；如果是左边有全程量词的存在量词，消去时该变量改写成为全程量词的函数。2)略去全程量词“”。简单地省略掉该量词。,例题2-2：将下式化为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)(x)(y)Q(y,b)R(x)第三步，全称量词左移，（利用分配律），得(x)(y)P(a,x,y)(y)(Q(y,b)R(x)第四步，变元易名，存在量词左移，直至所有的量词移到前面，得：(x)(y)P(a,x,y)(y)(Q(y,b)R(x)(x)(y)P(a,x,y)(z)(Q(z,b)R(x)=(x)(y)(z)(P(a,x,y)Q(z,b)R(x)由此得到前述范式。,第五步，消去“”，略去“”消去(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),2.3.2子句集,文字：不含任何连接词的谓词公式。子句：一些文字的析取（谓词的和）。子句集：所有子句的集合。对于任一个公式G，都可以通过Skolem标准形，标准化建立起一个子句集与之相对应。因为子句不过是一些文字的析取，是一种比较简单的形式，所以对G的讨论就用对子句集S的讨论来代替，以便容易处理。,子句集S的求取,子句集S可由下面的步骤求取：1.谓词公式G转换成前束范式2.消去前束范式中的存在变量，略去其中的任意变量，生成SKOLEM标准形3.将SKOLEM标准形中的各个子句提出，表示为集合形式。教师提示：为了简单起见，子句集生成可以理解为是用“，”取代SKOLEM标准形中的“”，并表示为集合形式。注意：SKOLEM标准形必须满足合取范式的条件。即，在生成子句集之前逻辑表达式必须是各谓词表达式或谓词或表达式的与。,定理：谓词表达式G是不可满足的，当且仅当其子句集S是不可满足的。,G与S并不等值，但它们在不可满足的意义下是一致的。因此如果要证明A1A2A3B，只需证明GA1A2A3B的子句集S是不可满足的。注意：G真不一定S真，而S真必有G真，即：SG。因为：在生成SKOLEM标准形时将存在量词用常量或其他变量的函数代替，使得变量讨论的论域发生了变化，即论域变小了。所以G不能保证S真。,谓词归结子句形,G=G1G2G3Gn的子句形G的子句集的求取过程可以分解成几个部分单独处理。如果Gi的子句集为Si，则有S=S1S2S3Sn，虽然G的子句集不为S，但是可以证明：SG与S1S2S3Sn在不可满足的意义上是一致的。即SG不可满足S1S2S3Sn不可满足由上面的定理，我们对SG的讨论，可以用较为简单的S1S2S3Sn来代替。为方便起见，也称S1S2S3Sn为G的子句形，即：SGS1S2S3Sn。,求取子句集的例子（1）,例23：对所有的x,y,z来说，如果y是x的父亲，z又是y的父亲，则z是x的祖父。又知每个人都有父亲，试问对某个人来说谁是它的祖父？求：用一阶逻辑表示这个问题，并建立子句集。解：这里我们首先引入谓词：P(x,y)表示x是y的父亲Q(x,y)表示x是y的祖父ANS(x)表示问题的解答,求取子句集的例子（2）,对于第一个条件，“如果y是x的父亲，z又是y的父亲，则z是x的祖父”，一阶逻辑表达式如下：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),x)对于结论：某个人是它的祖父B：(x)(y)Q(x,y)否定后得到子句：SB：Q(x,y)ANS(x)则得到的相应的子句集为：SA1，SA2，SB,2.4归结原理,本节在上节的基础上，进一步具体介绍谓词逻辑的归结方法。谓词逻辑的归结法是以命题逻辑的归结法为基础，在Skolem标准形的子句集上，通过置换和合一进行归结的。基本概念：一阶逻辑：谓词中不再含有谓词的逻辑关系式。个体词：表示主语或宾语的词谓词：刻画个体性质或个体之间关系的词量词：表示数量的词个体常量：a，b，c个体变量：x，y，z谓词符号：P，Q，R量词符号：，,2.4.1合一和置换,置换可以简单的理解为是在一个谓词公式中用置换项去置换变量。定义：置换是形如t1/vl,tn/vn的一个有限集。其中vi是变量而ti是不同于vi的项(常量、变量、函数),且vivj(ij),i,j=1,2,n例如a/x，c/y，f(b)/z是一个置换。g(y)/x，f(x)/y不是一个置换。（原因是它在x和y之间出现了循环置换现象。）不含任何元素的置换为空置换,以表示。置换可作用于某个谓词公式上,也可作用于某个项上。置换作用于一谓词公式E,结果以E表示,并称为E的一个例。作用于项t,结果以t表示。,定义：置换的乘法（合成）,设=t1/xl,tn/xn，=u1/y1,um/ym，是两个置换。则与的乘法（合成）也是一个置换，记作。它是从集合t1/xl,tn/xn，u1/y1,um/ym中删去以下两种元素：i.当ti=xi时，从中删除ti/xi(i=1,2,n);ii.当yix1,xn时，从中删除ui/yi(i=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/zf(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,合一,合一：合一可以简单地理解为“寻找相应变量的置换，使两个谓词公式一致”。定义：设有公式集EE1,Ek，若存在一个置换，可使E1=E2=Ek，则称是E的一个合一。同时称E1,Ek是可合一的。例：设有公式集FP(x,y,f(y),P(a,g(x),z)，则a/x,g(a)/y,f(g(a)/z是它的一个合一。注意：一般说来，一个公式集的合一不是唯一的。,最一般合一,定义：最一般合一设是公式集E1,Ek的一个合一置换，如果对E的任意一个合一都存在一个置换，使得，则称是E1,Ek的最一般合一（MostGeneralUnifier，简记为mgu）换句话来说，其他任何合一置换都是与某个置换的合成。一个公式集的最一般合一是唯一的。若用最一般合一去置换那些可合一的谓词公式，可使它们变成完全一致的谓词公式。归结原理方法与命题逻辑基本相同。但由于有变量与函数，所以要考虑合一和置换。,2.4.2归结式,在谓词逻辑下求两个子句的归结式，和命题逻辑一样是消互补对，但需考虑变量的合一与置换。设C1,C2是两个无公共变量的子句，L1、L2分别是C1、C2的文字，如果Ll与L2有mgu，则(C1-L1)(C2-L2)称作子句C1、C2的一个二元归结式，而L1、L2为被归结的文字。子句因子：如果一个子句C的几个文字有mgu，那么C的例C称作子句的因子（进行子句内部的化简）。,归结式的注意事项,1、谓词的一致性，P()与Q()，不可以归结。2、常量的一致性，P(a,)与P(b,.)，不可以归结。3、变量，P(a,.)与P(x,)，可以通过置换归结。4、变量与函数，P(a,x,.)与P(x,f(x),)，不可以归结；但P(a,x,)与P(x,f(y),)，可以通过对两式分别做f(y)/x置换和a/x，再归结。5、不能同时消去两个互补对，形如PQ与PQ得空，是不正确的。6、对子句集中的元素先进行内部简化（置换、合并），然后进行归结。,求谓词逻辑归结式的例子,例：设：C1P(y)P(f(x)Q(g(x)，C2P(f(g(a)Q(b)，求：C1和C2的归结式。解：对C1，取最一般合一f(x)/y，得C1的因子C1P(f(x)Q(g(x)对C1的因子和C2进行归结，可得到C1和C2的归结式：Q(g(g(a)Q(b),2.4.3归结过程,谓词逻辑的归结过程与命题逻辑的归结过程相比，其基本步骤相同，但每步的处理对象不同。谓词逻辑需要把由谓词构成的公式集化为子句集，必要时在得到归结式前要进行置换和合一。谓词逻辑归结过程：1、写出谓词关系公式2、用反演法写出谓词表达式3、化为SKOLEM标准形4、求取子句集S5、对S中可归结的子句做归结6、归结式仍放入S中，反复归结过程7、得到空子句命题得证,例题2-4：快乐学生问题,假设任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有的考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。求证：张是快乐的。解：（一）先将问题用谓词表示如下：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),（二）将上述谓词子句转换为Skolem标准形：由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)结论的否定（三）根据以上7条子句，归结如下：(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)归结,归结原理,1归结法的实质：归结法是仅有一条推理规则的推理方法。归结的过程是一个语义树倒塌的过程。2归结法的问题对于传统归结法，子句中有等号或不等号时，完备性不成立。即，传统的归结法不能处理相等的关系。Herbrand定理是归结原理的理论基础；而正是由于Herbrand定理的不实用性引出了可实用的归结法。,2.5归结过程控制策略,要解决的问题：归结方法的知识爆炸。（背景：当使用归结法时，若从子句集S出发做所有可能的归结，并将归结式加入S中，再做第二层这样的归结，直到产生空子句。）（后果：无控制的盲目全面归结导致大量的不必要的归结式的产生，更严重的是，它们又将产生下一层的更大量的不必要的归结式的产生。这种盲目的全面归结会产生组合爆炸问题。）控制策略的目的：归结点尽量少（给出控制策略，以使系统仅选择合适的子句对其做归结来避免多余不必要的归结式的出现，或者说少做些归结但仍然导出空子句来。）控制策略的原则：删除不必要的子句，或对参加归结的子句做限制。,控制策略的分类（1）删除策略（通过删除某些无用的子句来缩小归结的范围）删除策略包括：纯文字删除法、重言式删除法、包孕删除法（2）限制策略（通过对参加归结的子句进行某些限制来减少归结的盲目性）限制策略包括：线性归结、单元（单文字）归结、语义归结、输入归结和支持集策略等。,2.5.1删除策略,名词解释：归类：设有两个子句C和D，若有置换使得CD成立，则称子句C把子句D归类（也称C包孕于D）。（可以理解为，由于小的可以代表大的，所以小的吃掉大的了。）若对S使用归结推理过程中,当归结式Cj是重言式或Cj被S中子句或归结式Ci(i完备。（采用归结策略进行的归结过程没有破坏归结法的完备性。）,2.5.2采用支撑集策略名词解释：支撑集：设有不可满足子句集S的子集T，如果S-T是可满足的，则T是支持集。t2-4_swf.htm,采用支撑集策略时，从开始到得到的整个归结过程中，只选取不同时属于S-T的子句，在其间进行归结。就是说，至少有一个子句来自于支撑集T或由T导出的归结式。例如：A1A2A3B中的B可以作为支撑集使用。要求每一次参加归结的亲本子句中，只要有一个是有目标公式的否定（B）所得到的子句或者它们的后裔。支撑集策略的归结是完备的。同样，所有可归结的谓词公式都可以用采用支撑集策略达到加快归结速度的目的。问题是如何寻找合适的支撑集。一个最容易找到的支撑集是目标子句的非，即SB。,支持集策略的语义归结过程,例S=PQ,PR,QR,R取T=R支持集归结过程：(1)PQ(2)PR(3)QR(4)R(5)P(2)(4)(6)Q(3)(4)(7)Q(1)(5)(8)口(6)(7),2.5.3语义归结策略,语义归结策略是将子句S分成两部分，约定每部分内的子句间不允许做归结。还引入了文字次序，约定归结时其中的一个子句的被归结文字只能是该子句中“最大”的文字。例S=PQR,PR,QR,R1）规定S中出现的文字的次序为PQR。2）选取S的一个解释I=(P,Q,R)用它来将S分成两个部分。S1=PR,QR为在I下为假的子句集合S2=PQR,R为在I下为真的子句集合规定Si内部的子句不允许归结,S1与S2子句间的归结必须是S1中的最大文字方可进行。这样所得的归结式,仍按I来放入S1或S2。,3）归结过程：,(1)PQRS2(2)PRS1(3)QRS1(4)RS2(5)QR(2)(1)归结S2(6)PR(3)(1)归结S2(7)R(2)(6)归结S1(8)R(3)(5)归结S1(9)口(7)(4)归结,2.5.4线性归结策略线性归结完备图25线性归结策略示意图t2-5_swf.htm,线性归结策略首先从子句集中选取一个称作顶子句的子句C0开始作归结。归结过程中所得到的归结式Ci立即同另一子句Bi进行归结得归结式Ci+1。而Bi属于S或是已出现的归结式Cj(ji)。即，如图所示归结得到的新子句立即参加归结。线性归结是完备的。同样，所有可归结的谓词公式都可以采用线性归结策略达到加快归结速度的目的。如果能搞找到一个较好的顶子句，可以使归结顺利进行。否则也可能事与愿违。,例S=PQ，PQ，PQ，PQ,选取顶子句Co=PQ线性归结过程:(l)PQ(2)PQ(3)PQ(4)PQ(5)Q(1)(2)(6)P(5)(3)(7)Q(6)(4)(8)口(7)(5),2.5.5单元归结策略,单元归结策略要求在归结过程中，每次归结都有一个子句是单元子句（只含一个文字的子句）或单元因子。显而易见，词中方法可以简单地削去另一个非单子句中的一个因子，使其长度减少，构成简单化，归结效率较高。单元归结完备；反之不成立。初始子句集中没有单元子句时，单元归结策略无效。所以说反之不成立，即此问题不能采用单元归结策略。,单元归结的例子,例1S=PQ,PR,QR,R单元归结过程(1)PQ(2)PR(3)QR(4)R(5)P(4)(2)(6)Q(4)(3)(7)Q(5)(1)(8)P(6)(1)(9)R(7)(3)(10)口(7)(6),2.5.6输入归结策略,与单元归结策略相似，输入归结策略要求在归结过程中，每一次归结的两个子句中必须有一个是S的原始子句。这样可以避免归结出的不必要的新子句加入归结，造成恶性循环。可以减少不必要的归结次数。输入归结完备；反之不成立。如同单元归结策略，不是所有的可归结谓词公式的最后结论都是可以从原始子句集中的得到的。简单的例子，归结结束时，即最后一个归结式为空子句的条件是，参加归结的双方必须是两个单元子句。原始子句集中没有单元子句的谓词公式一定不能采用输入归结策略。,例2S=PQ,PR,QR，R输入归结过程(1)PQ(2)PR(3)QR(4)R(5)QR(1)(2)(6)R(3)(5)(7)口(4)(6),2.6Herbrand定理,Herbrand定理是归结原理的理论基础，归结原理的正确性是通过Herbrand定理来证明的。同时归结原理是Herbrand定理的具体实现，利用Herbrand定理对公式的证明是通过归结法来进行的。本节简单地描述了Herbrand定理的基本思想和相关预备知识，最后给出Herbrand定理的一般形式。定义：公式G永真：对于G的所有解释，G都为真。定义：公式G永假（矛盾）：没有一个解释使G为真。,2.6.1Herbrand定理概述,问题：一阶逻辑公式的永真性（永假性）的判定是否能在有限步内完成？1936年图灵(Turing)和邱吉(Church)互相独立地证明了：“没有一般的方法使得在有限步内判定一阶逻辑的公式是否是永真（或永假）。但是如果公式本身是永真（或永假）的，那么就能在有限步内判定它是永真（或永假）。对于非永真（或永假）的公式就不一定能在有限步内得到结论。判定的过程将可能是不停止的。”,2.6.1.1Herbrand定理思想,要证明一个公式是永假的，采用反证法的思想（归结原理），就是要寻找一个已给的公式是真的解释。然而，如果所给定的公式的确是永假的，就没有这样的解释存在，并且算法在有限步内停止。因为量词是任意的，所讨论的个体变量域D是任意的，所以解释的个数是无限、不可数的，要找到所有的解释是不可能的。Herbrand定理的基本思想是简化讨论域，建立一个比较简单、特殊的域，使得只要在这个论域上（此域称为H域），原谓词公式仍是不可满足的，即保证不可满足的性质不变。,2.6.1.2H域,H域的定义：设G是已给的公式,定义在论域D上,令H0是G中所出现的常量的集合。若G中没有常量出现,就任取常量aD,而规定H0=a。Hi=Hi-l所有形如f(t1,.,tn)的元素其中f(tl,tn)是出现于G中的任一函数符号,而t1,tn是Hi-1的元素,i=1,2,。规定H为G的H域(或说是相应的子句集S的H域)。不难看出，H域是直接依赖于G的，而且最多只有可数个元素。,H域和D域关系示意图如下图表示。图21H域与D域关系t2-1_swf.htm,H域例题,例题2-4：设子句集S=P(x),Q(y,f(z,b),R(a)，求H域解：H0a,b为子句集中出现的常量H1a,b,f(a,b),f(a,a),f(b,a),f(b,b)H2a,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=H1H2解毕。,原子集A,原子集A为公式中出现的谓词套上H域的元素组成的集合。A=所有形如P(t1,.,tn)的元素。这里，P(x1,xn)为出现于S中的任一谓词符号，而t1,.,tn为S的H域中的任意元素。即把H域中的东西填到S的谓词里去。上例题的原子集为：A=P(a),Q(a,a),R(a),P(b),Q(b,a),Q(b,b),Q(b,a),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上的真值可确定。不可数问题转化成为了可数问题。S中的谓词是有限的，H是可数的，因此，A也是可数的。,2.6.1.3H解释,解释I：谓词公式G在论域D上任何一组真值的指定称为一个解释。H解释：子句集S在H域上的解释称为H解释。I是H域下的一个指派。凡对A中各元素真假值的一个具体设定，都是S的一个H解释。由子句集S建立H域、原子集A，希望定义于一般论域D上使S为真的任一解释I，可由依于S的H域上的某个解释I*来实现。这样，便使任意论域D上S为真的问题，化成了仅有可数个元素的H域上S为真的问题了。从而子句集S在D上不可满足问题化成了H上的不可满足的问题。,几个术语的定义,没有变量出现的原子、文字、子句和子句集，分别称为基原子、基文字、基子句和基子句集。基例：子句集S中某子句C中所有变元符号均以S的H域中的元素代入时，所得的基子句C称为C的一个基例。若一个解释I*使得某个基子句为假，则此解释I*为假。,关于基例,例S=P(x),Q(f(y)R(y)有H=a,f(a),f(f(a),对任一bD,子句P(b),Q(f(b)R(b)都叫基子句。而P(a),P(f(a)都称作子句C=P(x)的基例。同样，Q(f(a)R(a),Q(f(f(a)R(f(a)都是子句Q(f(y)R(y)的基例。,例：SP(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),I1*，I2*，I3*中出现的P(a)表示P(a)的取值为T，出现的P(a)表示P(a)的取值为F。显然在H域上，这样的定义I*下，S的真值就确定了。如：S|I1*T，S|I2*F，S|I3*F这是因为子句集SP(x)Q(x),R(f(y)的逻辑含义为：(x)(y)(P(x)Q(x)R(f(y)，论域H为a,f(a),f(f(a),。,Herbrand定理（H解释）,关键问题：对于公式G的所有的解释，如果公式取值全为假，才可以判定G是不可满足的。因为所有解释代表了所有的情况，如果这些解释可以被穷举，问题便可解决。对论域D上的任一解释I,若有S|I=T,如何求得一个相应的H解释I*,使得S|I*=T成立。由I到I*,实为H域到D域的映射,对H中每个常量、每个函数依I来规定D中的一个确定的元素。,以下三个定理保证了归结法的正确性。定理2.3.2(1)设I是S的论域D上的解释,存在对应于I的H解释I*,使得若有S|I=T,必有S|I*=T。说明：由I到I*,实为H域到D域的映射。即：对H中每个常量、每个函数依I来规定D中的一个确定的元素。定理2.3.2(2)子句集S是不可满足的,当且仅当在所有的S的H解释下为假。说明：这个定理将S在一般论域D上的不可满足问题化成了可数集H上的不可满足问题。定理2.3.2(3)子句集S是不可满足的，当且仅当对每个解释I下,至少有S的某个子句的某个基例为假。解释：因为S的逻辑含义是所包含的子句的合取,而且变量受全称量词作用。那么在某个解释I(均指H解释)下为假,只需某个子句的某个基例为假,而S是不可满足则要求在任一解释下均为假。,2.6.2语义树与Herbrand定理,从几何上进行讨论，将子句集S的所有可能解释展示在一棵树上，进而观察每个分枝对应的S的逻辑真值是真是假。语义树的构成方法：原子集A中所有元素逐层添加到一棵二叉树，并将元素的是与非分别标记在两侧的分枝上。语义树特点：一般H是无限可数集，因此，S的语义树是无限树。,语义树的意义,语义树可以理解为H域的图形解释。通过子句集SH域原子集A语义树，可见，讨论的对象从无限、不可数论域D转换成了可数的、有序的语义树。建立语义树的目的：把S中的每个解释都摊开。S的完全语义树的每个直到叶结点N的分枝都对应于S的一个解释I(N)。讨论S的不可满足性，可通过对语义树的每个分枝计算S的每一个解释的真值而实现。如果每个基例都为假，则可认为是不可满足的。有时并非需要无限地延伸某个分枝方能确定在相应的解释下S取假值。如果某个分枝延伸到结点N时，I(N)已使S的某一子句的某一基例为假，就无需再对N作延伸了。,例1设子句集S的原子集A=P,Q,R,属命题逻辑。这时S的原子集就是S中出现的全体原子命题。为了方便,常用I(N34)=P,Q,R表示从根结点到结点N分枝上所标记的所有文字的并集。图2.1所示S的语义树是一棵有限树。,语义树中的几个定义,完全语义树：如果对一棵语义树的所有叶结点N来说,I(N)包含了S的原子集A=A1,A2,中的所有元素Ai或Ai（i=1n)，就称S是完全语义树。失败结点：如果结点N的I(N)使S的某一子句的某一基例为假,而N的父辈结点不能判断这个事实,就说N是失败结点。封闭树：如果S的完全语义树的每个分枝上都有一个失败结点,就说它是一棵封闭树。,例：SP(x)Q(x)，P(f(y)，Q(f(y)，画出其语义树。,解：子句集S的H域为：Ha，f(a)，f(f(a)，原子集为：AP(a),Q(a),P(f(a),Q(f(a),从A出发便可画出S的语义树，