《人工智能》第三章知识演绎课件

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,人工智能,第三章 知识演绎,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,主讲：夏幼明,人工智能,示范课程,2,规则演绎系统,谓词演绎的归结方法, 归结反驳搜索策略,Hone,子句的归结,“,知识演绎,”,核心内容,3,规则演绎系统,在基于规则系统中，每个,if,可能与某断言,(assertion),集中的一个或多个断言匹配；,then,部分用于规定放入工作内存的新断言。,这种系统叫做基于规则的演绎系统,(rule based deduction system),。,在这种系统中，通常称规则的,if,部分为前项,(antecedent),，称规则的,then,部分为后项,(consequent),。,4,规则演绎系统,基于规则的求解系统由,if-then,形式的规则,建立的。,例如：,if (antecedent) then (consequent),基于规则的系统称为规则演绎系统，若后件用于规定动作，则称为产生式系统。规则演绎系统可以分为如下的3种： 规则正向演绎系统、规则逆向演绎系统、规则双向演绎系统。,前件,后件,5,规则,演绎系统,(1),规则正向演绎系统,从,if,部分向,then,部分推理的过程称为正向推理，即从事实或状态向目标或行动进行操作。,规则正向演绎系统的步骤：,事实表达命题式的与或形变换,利用,(W1W2),和,(,W1W2),的等价关系，消去符号,(,如果存在该符号的话,),。实际上，在事实中间很少有符号出现，因为可把蕴涵式表示为规则。,用狄,摩根,(De Morgan),定律把否定符号移进括号内，直到每个否定符号的辖域最多只含有一个谓词为止。,6,规则,演绎系统,(1),规则正向演绎系统,从,if,部分向,then,部分推理的过程称为正向推理，即从事实或状态向目标或行动进行操作。,规则正向演绎系统的步骤：,x,y,P(,x,y,),事实表达命题式的与或形变换,x,P(,x,f,(,x,),y,x,P(,x,y,) ,x,P(,x,a,) ,x,P(,x,) ,x, P(,x,),对所得到的表达式进行,Skolem,化和前束化。,对全称量词辖域内的变量进行改名和变量标准化，而存在量词量化变量用,Skolem,函数代替。,删去全称量词，而任何余下的变量都被认为具有全称量化作用。,7,规则,演绎系统,(1),规则正向演绎系统,从,if,部分向,then,部分推理的过程称为正向推理，即从事实或状态向目标或行动进行操作。,规则正向演绎系统的步骤：,例,1,：我们有事实表达式,(,u)(,v)Q(v,，,u),(R(v)P(v)S(u,，,v),把它化为,：,Q(v,A),R(v),P(v),S(A,v),对变量更名标准化，使得同一变量不出现在事实表达式的不同主要合取式中。更名后得表达式：,Q(w,A),R(v),P(v),S(A,v),必须注意到,Q(v,，,A),中的变量,v,可用新变量,w,代替，而合取式,R(v),P(v),中的变量,v,却不可更名，因为后者也出现在析取式,S(A,v),中。,8,规则,演绎系统,(1),规则正向演绎系统,从,if,部分向,then,部分推理的过程称为正向推理，即从事实或状态向目标或行动进行操作。,规则正向演绎系统的步骤：,例,2,：我们有事实表达式,(,v) (,u) Q(v,，,u),(R(v)P(v)S(u,，,v),注意，这时变量,u,成为了变量,v,的函数,f,(v),，利用,Skolem,函数把这个表达式化为,：,Q(v,f,(v),R(v),P(v),S(,f,(v),v),9,规则,演绎系统,(1),规则正向演绎系统,规则正向演绎系统的步骤：,事实表达命题式的与或形变换,R(V),P(V),R(V) ,P(V),S(A,V),R(V) ,P(V),S(A,V),Q(W,A),Q(W,A),R(V) ,P(V),S(A,V),每个节点表示该事实表达式的一个子表达式。某个事实表达式,(E,1,E,n,),的每个合取子表达式,E,1,，,，,E,n,是用后继节点表示的，并由一个,k,线连接符把它们连接到父辈节点上。某个事实表达式,(E,1,E,k,),的析取关系子表达式,E,1,，,，,E,k,是由单一的后继节点表示的，并由一个单线连接符接到父辈结点。,10,规则,演绎系统,(1),规则正向演绎系统,与或图的正向推理：,限制规则的公式类型为：,L,W,其中：,L,为单文字；,W,为与或形的唯一公式。,例如：考虑规则,S,(,x,y,),z,应用到右面的事实表达式中。,T,S,(T U),S (T U),(P Q) R S (T U),(P Q),R,P,Q,U,(P Q) R,表示某个事实表达式的与或图的叶节点均由表达式中的文字来标记。,图中标记有整个事实表达式的节点，称为根节点，它在图中没有祖先。,X,Y,S,XY,Z,当目标公式按正向规则应用到事实表达式与或图，产生的与或图包含有终止在目标节点的一个解图时，证明目标公式成立。,11,规则,演绎系统,(1),规则正向演绎系统,与或图的正向推理：,公式的与或图表示有个有趣的性质，即由变换该公式得到的子句集可作为此与或图的解图的集合,(,终止于叶节点,),读出；也就是说，所得到的每个子句是作为解图的各个叶节点上文字的析取。这样，由表达式,Q(w,A),R(v),P(v),S(A,v),得到的子句为：,Q(w,A),S(A,v),R(v),S(A,v),P(v),我们一般把事实表达式的与或图表示倒过来画，即把根节点画在最下面，而把其后继节点往上画。我们将要讨论到目标公式的与或图表示，它是按通常方式画出的，即目标在上面。,12,规则,演绎系统,(1),规则正向演绎系统,推理规则：消解,(,归结,),把原子公式和原子公式的否定称为文字。任何文字的析取式称为子句。析取式,P Q R,可用子句表示为：,P,，,Q,，,R,。不包含任何文字的子句称为空子句（,NIL,）。空子句是永假的。由子句构成的集合称为子句集。,归结定义为：从, 1,和, 2(1,和,2,是文字集合，是一个文字,),，可以归结为,1 2,，它被称为两个子句的归结式。 是被归结的文字。这个过程称为归结。,13,规则,演绎系统,(1),规则正向演绎系统,推理规则：消解,(,归结,),归结定义为：从, 1,和, 2(1,和,2,是文字集合，是一个文字,),，可以归结为,1 2,，它被称为两个子句的归结式。 是被归结的文字。这个过程称为归结。例：,1,、,P R,和,Q R,归结,R,为,P Q,。注意到,P R,与,Q R,的等价写法为, P R,、,R Q,，利用蕴涵“”的传递性，则有, P Q,，而它的等价表示为,P Q,。于是，可以看出，通过链式的推理规则产生的结果与归结是一致的。,2,、,R,和,Q R,归结,R,为,Q,。而,Q R,等价于,R Q,，这样，此归结与假言推理是一致的。,14,规则,演绎系统,(1),规则正向演绎系统,推理规则：消解,(,归结,),归结是合理的。,证明：所谓合理的，就是说，如果, 1,和, 2,均是真的，那么,1 2,是真的。对的真假值讨论就可以了。,情形一： 是真的，那么，,是假的，因此，, 2,为真，必须,2,为真，故,1 2,是真的。,情形二： 是假的，那么，, 1,为真，必须,1,为真，故,1 2,是真的。,综合情形一和二，可知， ,1,、,2,至少有一个必须为真，即,1 2,是真的。,15,规则,演绎系统,(1),规则正向演绎系统,与或图的正向推理：,应用消解原理的结果:,规则S (,X,Y,),Z,化为子句：,S ,X,Z,；,S ,Y,Z,；,事实表达式(P Q) R S (T U)化为,子句：P Q S； RS； PQTU； RTU,归结结果：X Z P Q；Y Z P Q；,R X Z；RYZ,16,规则,演绎系统,(1),规则正向演绎系统,与或图的正向推理：,应用一条规则得到的与或图继续表示事实表达式和推得的表达式，这可利用匹配弧两侧有相同标记的节点来实现。对一个节点应用一条规则之后，此节点就不再是该图的叶节点。,不过，它仍然由单一文字标记而且可以继续具有一些应用于它的规则。,我们把图中标有单文字的任一节点都称为文字节点，由一个与或图表示的子句集就是对应于该图中以文字节点终止的解图集。,17,规则,演绎系统,(1),规则正向演绎系统,作为终止条件的目标公式,应用规则推理的目的在于从某个事实公式和某个规则集出发来证明某个目标公式。,在正向推理系统中，这种目标表达式只限于可证明的表达式，尤其是可证明的文字析取形的目标公式表达式。我们用文字集表示此目标公式，并设该集各元都为析取形式。,目标文字和规则可用来对与或图添加后继节点，当一个目标文字与该图中文字节点,n,上的一个文字相匹配时，我们就对该图添加这个节点,n,的新后裔，并标记为匹配的目标文字。这个后裔叫做目标节点，目标节点都用匹配弧分别接到它们的父辈节点上。,18,规则,演绎系统,(1),规则正向演绎系统,作为终止条件的目标公式,例,3,：事实PQ； 规则P C，QG；目标CG。,把规则化为子句形，得子句集：,P ,C，,Q,G,目标的否定为,:,(CG),；其子句形为,:,C,，,G,P ,C,P ,Q,Q,C,C,Q,Q,G,G,Q,NIL,19,规则,演绎系统,(1),规则正向演绎系统,作为终止条件的目标公式,例,3,：事实PQ； 规则P C，QG；目标CG。,P,Q,P,R,(,P,Q,),(,P,O,),R,S (T U) (P Q) R,(,T,U,),S,T,U,Q,(,T,U,) ,S,C,D,E,G,C,G,当目标公式按正向规则应用到事实表达式与或图，产生的与或图包含有终止在目标节点的一个解图时，证明目标公式成立。,20,规则,演绎系统,(2),规则,逆向演绎系统,基于规则的逆向演绎系统，其操作过程与正向演绎系统相反，即为从目标到事实的操作过程，从,then,到,if,的推理过程。,目标表达式的与或形式,采用与变换事实表达式同样的过程，把目标公式化成与或形，即消去蕴涵符号，把否定符号移进括号内，对全称量词,Skolem,化并删去存在量词。留在目标表达式与或形中的变量假定都已存在量词量化。,例,1,：目标表达式：,(,y,)(,x,)P(,x,) ,(,x,y,),P(,x,)S(,y,),被化成与或形：,P(,f,(,y,)Q(,f,(,y,),y,),P(,f,(,y,),S(,y,),式中，,x,=,f,(,y,),为一,Skolem,函数。,21,规则,演绎系统,(2),规则,逆向演绎系统,目标表达式的与或形式,与或形的目标公式也可以表示为与或图。不过，与事实表达式的与或图不同的是，对于目标表达式，与或图中的,k,线连接符用来分开合取关系的子表达式。在目标公式的与或图中，我们把根节点的任一后裔叫做子目标节点，而标在这些后裔节点中的表达式叫做子目标。,例,1,：目标表达式：,P(,f,(,y,)Q(,f,(,y,),y,),P(,f,(,y,),S(,y,),P(,f,(,y,)Q(,f,(,y,),y,),P(,f,(,y,),S(,y,),Q(,f,(,y,),y,),P(,f,(,y,),S(,y,),P(,f,(,y,),Q(,f,(,y,),y,),S(,y,),P(,f,(,y,),P(,f,(,y,),S(,y,),22,规则,演绎系统,(2),规则,逆向演绎系统,与或图的逆向推理规则变换,我们应用逆向推理规则来变换逆向演绎系统的与或图结构，逆向推理规则是建立在确定的蕴涵式基础上的，现在把这些逆向推理规则限制为,:,W L 其中：W为任一与或形公式，L为单文字。,逆向系统中的事实表达式均限制为文字合取形，它可以表示为一个文字集。当一个事实文字和标在该图文字节点上的文字相匹配时，就可把相应的后裔事实节点添加到该与或图中去。这个事实节点通过标有,mgu,的匹配弧与匹配的子目标文字节点连接起来。同一个事实文字可以多次重复使用,(,每次用不同变量,),，以便建立多重事实节点。,23,规则,演绎系统,(2),规则,逆向演绎系统,与或图的逆向推理规则变换,事实:,F1:DOG(FIDO);,狗的名字叫,Fido,F2:,BARKS(FIDO);,Fido,是不叫的,F3:WAGS-TAIL(FIDO);,Fido,摇尾巴,F4:MEOWS(MYRTLE);,猫咪的名字叫,Myrtle,规则:,R1:WAGS-TAIL(,x,1) DOG(,x,1)FRIENDLY(,x,1),摇尾巴的狗是温顺的狗,24,规则,演绎系统,(2),规则,逆向演绎系统,与或图的逆向推理规则变换,规则:,R2: FRIENDLY(,x,2),BARKS(,x,2) ,AFRAID(,y,2,x,2),温顺而又不叫的东西是不值得害怕的,R3: DOG(,x,3) ANIMAL(,x,3),狗为动物,R4:CAT(,x,4) ANIMAL(,x,4),猫为动物,R5:MEOWS(,x,5) CAT(,x,5),猫咪是猫,目标:(,x,)(,y,)CAT(,x,) DOG(,y,) ,AFRAID(,x,y,),是否存在这样的一只猫和一条狗，使得这只猫不怕这条狗,?,25,规则,演绎系统,(2),规则,逆向演绎系统,与或图的逆向推理规则变换,CAT(,x,) DOG(,y,) ,AFRAID(,x,y,),CAT(,x,),DOG(,y,),AFRAID(,x,y,),CAT(,x,5,),AFRAID(,x,2,y,2,),MEOWS(,x,),FRIENDLY(,y,),WAGS-TAIL(,y,),DOG(,x,1),FRIENDLY(,x,1,),BARKS(,y,),DOG(,FIDO,),MEOWS(MYRTLE),BARKS(,FIDO,),WAGS-TAIL(FIDO),DOG(,FIDO,),R1,R2,R5,x5,/,x,MYRTLE/,x,FIDO/,y,FIDO/,y,x2,/,x,，,y2,/,y,FIDO/,y,FIDO/,y,y,/,x,1,26,规则,演绎系统,(2),规则,逆向演绎系统,与或图的逆向推理规则变换,正向演绎系统能够处理任意形式的,if,表达式，但被限制在,then,表达式为由文字析取组成的一些表达式。逆向演绎系统能够处理任意形式的,then,表达式，但被限制在,if,表达式为文字合取组成的一些表达式。,CAT(MYRTLE)DOG(FIDO),AFRAID(MYRTLE,FIDO),27,谓词演绎的归结方法,谓词、函数、量词,谓词：表示个体对象之间的关系、属性或状态。其表示形式如下：,P(x1,x2,x3,.xn),其中：,P,是谓词符号，表示,x1,x2,x3,.xn,个体对象之间的属性、状态或关系。,x1,x2,x3,.xn,是谓词的参量（或称项），一般表示个体，它可以是个体常量、个体变量或是个体函数。个体变元的变化范围称为个体域（或论域）,例：,P(x):,表示,x,是素数,FRIEND(a,b),：表示,a,和,b,是朋友,28,谓词演绎的归结方法,谓词、函数、量词,个体函数：表示项之间的关系 有了个体函数之后，谓词的表达能力更强。假如个体函数,father(b),表示“个体,b,的父亲”，则谓词,FRIEND(a,father(b),表示“,a,和,b,的父亲是朋友”，显然表达能力更强了。,例：,E(x,y):,表示,x,和,y,相等关系 个体函数,square(x),：表示个体,x,的平方 则谓词,E(square(a),b),表示什么？,29,谓词演绎的归结方法,谓词、函数、量词,量词 全称量词：“所有”,“,一切”,“,任一”,“,全体”,“,凡是”等词称为全称量词，记为,存在量词：“存在”、“有些”、“至少有一个”、“有的”等词统称为存在量词，记为,例：,谓词,M(x):,表示,x,是人，谓词,N(x):,表示,x,有名字，则,x(M(x)N(x),表示“凡是人都有名字”。 谓词,G(x):,表示,x,是整数，,E(x),：表示,x,是偶数，则,x,（,G(x),E(x),表示“存在不是偶数的整数” 知识“不存在最大的整数”的表示 ：谓词,D(x,y),表示,x,大于,y,。则表示如下：,x(G(x),y(G(y)D(x,y),30,谓词演绎的归结方法,命题逻辑中的归结推理方法,若命题逻辑描述的命题,A1,A2,.An,和,B,要证明在,A1A2.An,成立的条件下有,B,成立，或说,A1A2.AnB,。很显然,A1A2.AnB,等价于证明,A1A2.An,B,是矛盾,(,永假,),式。归结推理的方法就是从,A1A2.An,B,出发使用归结推理规则来寻找矛盾，从而证明,A1A2.AnB,的成立。这种方法称为反演推理方法。,31,谓词演绎的归结方法,命题逻辑的归结推理过程,利用逻辑蕴含式和逻辑等价式将命题公式化成合取范式,(,子句的合取,),子句集：将若干个子句的合取式中的合取词换成逗号，形成的集合称为子句集。,从子句集,S,出发，仅只对,S,的子句间使用归结推理规则（即求归结式），并将所得归结式仍放入,S,中，进而再对新子句集使用归结推理规则，重复这些步骤直到得到空子句（说明有矛盾）。也就是说,S,是不可满足的，从而与子句集,S,对应的定理是成立的。,32,谓词演绎的归结方法,谓词公式的子句形,合取范式和析取范式,合取范式：,若谓词公式,A,有如下形式,B1B2.Bn,其中,Bi(i=1,2,.n),形如,L1L2.Ln,，并且,L1,L2,.Ln,都是文字。,析取范式：,若谓词公式,A,有如下形式,B1B2.Bn,其中,Bi(i=1,2,.n),形如,L1L2.Ln,，并且,L1,L2,.Ln,都是文字。,前束范式：,将所有的量词都放在谓词公式的前面。前束范式可分成前束合取范式和前束析取范式。,33,谓词演绎的归结方法,化成前束合取范式的步骤,Step1,：消去，,以外的连接词,A,B.,AB A,B.(,AB)(,BA),step2,：将连接词,内移，移到原子公式之前,(,A),A,(AB),A,B,(AB),A,B,xA(x),x,A(x),xA(x),x,A(x),34,谓词演绎的归结方法,化成前束合取范式的步骤,Step3,：将量词尽可能向左推，推到前缀所在的位置，用下列公式：,xA(x)B.,x,（,A(x)B,），其中,B,中不含约束变元,B,xA(x).,x,（,BA(x),），其中,B,中不含约束变元,xA(x)B.,x,（,A(x)B,），其中,B,中不含约束变元,B,xA(x).,x,（,BA(x),），其中,B,中不含约束变元 同样对上面式子中的改为可得到另一组关于的的替换式。,35,谓词演绎的归结方法,化成前束合取范式的步骤,step4,：用下式进行替换：,xA(x),xB(x).,x,（,A(x)B(x),）,xA(x),xB(x).,x,y,（,A(x)B(y),）,采用更名规则,xA(x),xB(x).,x,（,A(x)B(x),）,xA(x),xB(x).,x,y,（,A(x)B(y),）,采用更名规则,Step5,：使用，的分配律化成合取范式。,36,谓词演绎的归结方法,将谓词公式化成子句集的步骤,按上述步骤化成前束合取范式；,化成,Skolem,标准型，消去存在量词；消取存在量词时，还要进行变元替换。变元替换分两种情况：,若该存在量词在某些全称量词的辖域内，则用这些全称量词指导变元的一个函数代替该存在量词辖域中的相应约束变元，这样的函数称为,Skolem,函数；,若该存在量词不在任何全称量词的辖域内，则用一个常量符号代替该存在量词辖域中相应约束变元，这样的常量符号称为,Skolem,常量。,37,谓词演绎的归结方法,将谓词公式化成子句集的步骤,消去所有全称量词,消去合取词，用逗号代替，以子句为元素组成一个集合,S,，即是谓词公式的子句集。,38,谓词演绎的归结方法,引入控制策略,从谓词逻辑的归结方法中我们可以看出，当使用归结法时，若从子句集,S,出发做所有可能的归结，并将 归结式加入,S,中，再做第二层这样的归结，,直到产生空子 句。,这种盲目的归结，会产生组合爆炸问题。 这种无控制的归结导致大量的不必要的归结式的产生。,如何给出控制策略，以使系统仅 选择合式的子句对其做归结来避免多余不必要的归结式的 出现，或者说少做些归结但仍然导出空子句来，这已经成为 一个重要的问题。,39,谓词演绎的归结方法,引入控制策略,归纳起来，归结过程策略控制的要点如下：,要解决的问题：归结方法避免知识爆炸。,控制策略的目的：归结点尽量少。,控制策略的原则：删除不必要的子句，或对参加归结 的子句做限制。,给出控制策略，以使仅选择合式的子句对其做归结。 避免多余的、不必要的归结式出现。,40,谓词演绎的归结方法,引入控制策略,置换与合一(含有变量的归结式),在谓词逻辑中，有些推理规则可应用于一定的合式公式或合式公式集，以产生新的合式公式。,一个重要的推理规则是假言推理，这就是由合式公式,W1,和,W1=W2,产生合式公式,W2,的运算。,另一个推理规则叫做全称化推理，它是由合式公式,(,x)W(x),产生合式公式,W(A),，其中,A,为任意常量符号。,41,谓词演绎的归结方法,引入控制策略,置换与合一(含有变量的归结式),在谓词逻辑中，有些推理规则可应用于一定的合式公式或合式公式集，以产生新的合式公式。,一个重要的推理规则是假言推理，这就是由合式公式,W1,和,W1=W2,产生合式公式,W2,的运算。,另一个推理规则叫做全称化推理，它是由合式公式,(,x)W(x),产生合式公式,W(A),，其中,A,为任意常量符号。,综合推理：它是由合式公式,(,x) W1 (x) =W2 (x),，,W1(A),产生合式公式,W2(A),，其中,A,为任意常量符号。,42,谓词演绎的归结方法,引入控制策略,置换与合一,一个表达式的项可以是常量、变量和函数。合一就是寻找项对变量的置换而使表达式一致。,置换可用有序对的集合,s=,t,1,/,v,1,t,2,/,v,2,t,n,/,v,n,表示，其中,t,i,/,v,i,表示每个变量,v,i,用,t,i,替换。,t,i,可以是常量或变量或函数。,但是,f,(,v,i,),/,v,i,是不允许的，即在替换中不允许在项中出现被替换的变量。,置换是可以结合的，换句话说，如果,s1,和,s2,是合式公式,E,的置换，那么,(E)s1s2=(E)s1)s2,43,谓词演绎的归结方法,引入控制策略,置换与合一,把置换,s,作用于集合,E,i,中的每个公式得到的例的集合用,E,i,s,表示。如果存在一个置换,s,，使得,(E,1,)s = (E,2,)s = =(E,n,)s,，那么称公式集合,E,i,为可合一的，置换,s,称为,E,i,的合一者。,下面是递归合一算法,UNIFY(E,1,E,2,),；其中，,E,1,E,2,是待合一的公式：,1,、如果,E1,或,E2,是原子公式，无妨设是,E1,则执行,2,2,、如果,E1,和,E2,是相同的，,return NIL,3,、如果,E1,是一个变量则执行,4,否则到,6,4,、如果,E1,出现在,E2,中则,return FAIL,5,、,return E2 /E1,6,、,F1,E1,的第一个元素，,T1,E1,的其余元素；,F2,E2,的第一个元素，,T2,E2,的其余元素；,7,、,Z1,UNIFY(F1,F2),8,、如果,Z1=FAIL,则,returnFAIL,9,、,G1 Z1,作用于,T1,的结果；,G2 Z1,作用于,T2,的结果；,10,、,Z2,UNIFY(G1,G2),11,、如果,Z2=FAIL,则,returnFAIL,；否则,return Z1,与,Z2,的合成。,44,谓词演绎的归结方法,在谓词逻辑中，子句含有变量。这时，寻找一个置换，作用于给定的两个子句，使它们包括互补文字，即存在文字,1,和,1,，,然后进行归结。,设,C1,和,C2,是两个没有相同变量的子句，并分别表示成两个文字集合,Li,和,Mi,，,li,是,Li,的一个文字，,mi,是,Mi,的一个子集。若存在,s,是文字,li,和,mi,的最小合一置换，则,C12= Li-li,Mi- mis,，为子句,C1,和,C2,的归结。,更一般定义为：,设,C1,和,C2,是两个没有相同变量的子句，并分别表示成两个文字集合,Li,和,Mi,，,li,是,Li,的一个子集，,mi,是的一个子集,Mi,。若,s,是集合,li,和,mi,的并集的最小合一置换，则称,C12= Li-li,Mi-mi s,为,C1,和,C2,的归结。,45,谓词演绎的归结方法,等式谓词,在归结的过程中，通常谓词名的语义并不能真正获取，因此，有时无法得到正确的结论。例如：假设有,Equals(A,B),，但是，无法归结：,P(A,B),和,P(B,A),。因此，需要引入等式谓词：,自反性：,(,x),Equals(x,x),对称性：,(,x,y),Equals(x,y),Equals(y,x),传递性：,(,x,y,z),Equals(x,y),Equals(y,z),Equals(x,z),46,谓词演绎的归结方法,等式谓词,在归结的过程中，通常谓词名的语义并不能真正获取，因此，有时无法得到正确的结论。即使有等式谓词有了这些公理，但还是无法得到，例：,P(A),，,Equals(A,B),P(B),。,于是，我们给出等价替换规则：,假如有两个子句：,1,，,2,。 ,1 =() 1,， ,2 =,Equals(,), 2,其中， ，是项。 ,1,和,2,子句。 ,(),是包含的文字。如果有一置换使得，能够合一，那么有,1,和,2,的调解式：,= ( ) 1 2 ,该调解式实际上，是将中用替换，并且与,1 ,和 ,2 ,做析取。,47,归结反驳搜索策略,排序策略,定义,n,层归结项：,1,）把原子的子句称为,0,层归结项；,2,）,i+1,层的归结项是一个,i,层归结项和一个,j,层归结项归结的结果。,广度优先：按照归结项的层数每次产生该层的所有归结项，逐层生成，直到或者产生了空子句，或者不能再产生新的层次。,深度优先：首先产生一个第,1,层的归结项，然后，用某些第,1,层的归结项或,0,层归结项产生第,2,层的归结项，依次类推。,排序归结的一个通用策略是单元优先策略：这种归结至少有一个子句有一个单一的文字构成。这样的子句称为单元子句。,48,归结反驳搜索策略,精确策略,支持集的概念：子句,2,是另一个子句,1,的后裔，当且仅当：,(a),2,是,1,和另一些子句的一个归结项；或,(b) 2,是,1,的后裔与另一些子句的一个归结项。,2,是,1,的后裔，那么,1,是,2,的祖先。支持集定义为由一些子句组成，这些子句或来源于待证定理的否定，或者是这些子句的后裔。,支持集策略：只允许这样一些归结：在其中正在被归结的子句中的一个在支持集中。支持集策略是反驳完备的。即，假如只对一个不可满足的子句集合运用支持集归结，那么最终能导出空子句。,49,归结反驳搜索策略,精确策略,支持集的概念：子句,2,是另一个子句,1,的后裔，当且仅当：,(a),2,是,1,和另一些子句的一个归结项；或,(b) 2,是,1,的后裔与另一些子句的一个归结项。,2,是,1,的后裔，那么,1,是,2,的祖先。支持集定义为由一些子句组成，这些子句或来源于待证定理的否定，或者是这些子句的后裔。,线性输入策略：只允许这样的归结：其中至少有一个正被归结的子句是原始子句集的一个成员。线性输入策略不是反驳完备的。,祖先过滤策略：只允许这样一些归结：在其中至少有一个正被归结的子句的一个或者是原始子句集的一个或者是正被归结的别的子句的祖先。此策略是反驳完备的。,50,Hone,子句的归结,Horn,子句,Horn,子句是至多只有一个肯定文字的子句。,有三种类型的,Horn,子句：,一个单一原子，常被称为事实。,一个蕴含，常被称为规则，其条件和结论都是有一个肯定文字组成。,一个否定文字的集合，表示为结论为空，条件为合取肯定文字组成。这类子句常被称为“目标”,对于,Horn,子句的归结，存在着线性时间的演义算法。,51,Hone,子句的归结,Horn,子句,Horn,子句形成,PROLOG,语言的基础。,PROLOG,的推理由试图证明一个目标组成，推理的过程是执行一个,PROLOG,语言描述的程序。证明是通过对事实、目标和规则进行归结完成的。每个归结在一个目标与事实或规则之间进行的。,目标与事实进行归结：将目标的一个文字与事实进行合一。归结式是由初始目标中其他文字的所有置换得到新目标。,目标与规则进行归结：将目标的一个文字与规则的结论进行合一。归结式是把规则条件的所有文字的置换作成新目标。,52,Hone,子句的归结,Horn,子句,Horn,子句形成,PROLOG,语言的基础。,PROLOG,的推理由试图证明一个目标组成，推理的过程是执行一个,PROLOG,语言描述的程序。,在,PROLOG,程序中，子句的排序方式：,第一个子句是目标子句，接着是事实，最后是规则。,归结策略：通过顺序中的目标文字，检查排序的每个子句，执行第一个可能的归结来检查与目标的归结，然后从新的目标子句开始。当应用一个归结产生的子句为空时，一个目标子句的证明成功。如果对于一个目标子句所有归结都尝试，但是没有任何结果时，则目标子句不能证明。这时，需要进行回溯，到它前一个子目标，对此子目标进行其他归结，如果有新结果，则对下一个目标重新归结。,53,Hone,子句的归结,Horn,子句,Horn,子句形成,PROLOG,语言的基础。,PROLOG,的推理由试图证明一个目标组成，推理的过程是执行一个,PROLOG,语言描述的程序。,PROLOG,推理的例子,(,不含变量,),：,1),目标：,(,手臂可移动,) :-MOVES,2),事实：,(,电池已充电,)BAT_OK:-,3),事实：,(,积木可被举起,)LIFTABLE:-,4),规则：,(,如果电池已充电并且积木可被举起，那么，手臂可移动,),MOVES :-BAT_OK,，,LIFTABLE,1),和,4),归结得到新的目标为：,:- BAT_OK,，,LIFTABLE,。,此目标和,2),归结，合一，产生新的目标，,:- LIFTABLE,。,再与,3),归结得到空子句。,谢谢！,