清华大学《人工智能导论》课程电子教案（二）.ppt

单击此处编辑母版标题样式,*,*,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,第四章 谓词演算及应用,是一种形式语言，具有严密的理论体系,是一种常用的知识表示方法,例：,City（北京）,City（上海）,Age（张三，23）,(x)(y)(z)(F(x,y)F(y,z)GF(x,z),1,4.1 归结原理,归结原理是一种定理证明方法，1965年由Robinson提出，从理论上解决了定理证明问题。,归结原理的提出，对机器定理证明问题起到了推动作用。,2,子句集,无量词约束,元素只是文字的析取,否定符只作用于单个文字,元素间默认为合取,例：I(z),R(z),I(A),R(x)L(x),D(y),3,化子句集的方法,例：(,z)(x)(y)(P(x)Q(x)R(y)U(z),1,消蕴涵符,理论根据：a,b=a b,(,z)(x)(y),(P(x)Q(x)R(y),U(z),2,移动否定符,理论根据：(a b)=a b,(a b)=a b,(x)P(x)=(x)P(x),(x)P(x)=(x)P(x),(,z)(x)(y),(P(x)Q(x)R(y),U(z),4,化子句集的方法（续1）,3,变量标准化,即：对于不同的约束，对应于不同的变量,(,x)A(x)(x)B(x)=,(,x)A(x)(y)B(y),4,量词左移,(,x)A(x)(y)B(y)=,(,x)(y)A(x)B(y),5,消存在量词(skolem化）,原则：对于一个受存在量词约束的变量，如果他不受全程量词约束，则该变量用一个常量代替，如果他受全程量词约束，则该变量用一个函数代替。,(,z)(x)(y)(P(x)Q(x)R(y)U(z),=(x)(P(x)Q(x)R(,f(x),)U(,a,),5,化子句集的方法（续2）,6,化为合取范式,即(a,b)(cd)(ef),的形式,(x)(P(x)Q(x)R(f(x)U(a),=(x)(P(x)Q(x)R(f(x)U(a),=(x)P(x),R(f(x),U(a),Q(x),R(f(x),U(a),7,隐去全程量词,P(x)R(f(x)U(a)Q(x)R(f(x)U(a),6,化子句集的方法（续3）,8,表示为子句集,P(x)R(f(x)U(a),Q(x)R(f(x)U(a),9,变量标准化（变量换名）,P(x1)R(f(x1)U(a),Q(x2)R(f(x2)U(a),7,归结原理,定理：,若S是合式公式F的子句集，则F永假的充要条件是S不可满足。,S,不可满足：若nilS，则S不可满足。,8,使用归结原理证明定理的思路,目标的否定连同已知条件一起，化为子句集，并给出一种变换的方法，使得 S,S,1,S,2,.S,n,同时保证当S,n,不可满足时，有S不可满足。,9,4.2 归结方法（命题逻辑）,设子句：C,1,=L,C,1,C,2,=(L),C,2,则归结式C为：C=C,1,C,2,定理：,子句集S=C,1,C,2,C,n,与子句集S,1,=,C,C,1,C,2,C,n,的不可满足性是等价的。其中，C是C,1,和C,2,的归结式。,10,归结的例子,设公理集：,P,(P,Q)R,(ST)Q,T,求证：R,子句集：,(1)P,(2)PQR,(3)SQ,(4)TQ,(5)T,(6)R（目标求反）,化子句集：,(P,Q)R,=(PQ)R,=PQR,(ST)Q,=(ST)Q,=(ST)Q,=(SQ)(TQ),=SQ,TQ,11,子句集：,(1)P,(2)PQR,(3)SQ,(4)TQ,(5)T,(6)R（目标求反）,归结：,(7),PQ (2,6),(8)Q (1,7),(9)T (4,8),(10)nil (5,9),12,4.3 谓词逻辑的归结原理,问题：如何找归结对,例：P(x),Q(y),P(f(y),R(y),P(A),Q(y),P(f(y),R(y),基本概念,置换,s=t,1,/v,1,t,2,/v,2,t,n,/v,n,对公式E实施置换s后得到的公式称为E的例，记作E,s,。,例：s1=z/x,A/y,则：,Px,f(y),B,s,=Pz,f(A),B,13,合一,如果存在一个S置换，使得E,i,中 E,1s,=E,2s,=E,3s,=E,ns,，则称E,i,是可合一的。S为E,i,的合一者。,例：P(x,f(y),B),P(z,f(B),B),置换s=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),置换s=z/x,B/y和置换s=x/z,B/y也都是这两个谓词公式的合一者。,结论：合一者不唯一。,14,最一般合一者（mgu）,置换最少，限制最少，产生的例最具一般性。,如前面的例子：,P(x,f(y),B),P(z,f(B),B),对于置换,A/x,B/y,A/z，产生的例是：,P(A,f(B),B),对于置换=z/x,B/y，产生的例是：,P(z,f(B),B),mgu,也不是唯一的。,15,合一算法,例：P(x,x,z),P(f(y),f(B),y),前缀表示：,(P,x,x z),(P,(f y),(f B)y),置换：(f y)/x,(P(f y)(f,y,)z),(P(f y)(f,B,)y),置换：B/y,并使得(f B)/x,(P(f B)(f B),z,),(P(f B)(f B),B,),置换：B/z,得到置换：(f B)/x，B/y，B/z,置换后的结果：,(P(f B)(f B)B),16,谓词逻辑的归结方法,对于子句C,1,L,1,和C,2,L,2,，如果L,1,与L,2,可合一，且s是其合一者，则(C,1,C,2,),s,是其归结式。,例：,P(x),Q(y),P(f(z),R(z),=Q(y)R(z),17,归结举例,设公理集：,(,x)(R(x)L(x),(x)(D(x)L(x),(x)(D(x)I(x),求证：(x)(I(x)R(x),化子句集：,(,x)(R(x)L(x),=,(,x)(R(x)L(x),=R(x)L(x)(1),18,(x)(D(x)L(x),=(x)(D(x)L(x),=D(x)L(x)(2),(x)(D(x)I(x),=D(A)I(A),=D(A)(3),I(A)(4),19,目标求反：,(x)(I(x)R(x),=(x)(I(x)R(x),=(x)(I(x)R(x),=I(x)R(x)(5),换名后得字句集：,R(x,1,)L(x,1,),D(x,2,)L(x,2,),D(A),I(A),I(x,5,)R(x,5,),20,例题的归结树,R(x,1,)L(x,1,),D(x,2,)L(x,2,),D(A),I(A),I(x,5,)R(x,5,),I(A),I(x,5,),R(x,5,),R(A),A/x5,R(x,1,),L(x,1,),L(A),A/x,1,D(x,2,),L(x,2,),D(A),A/x,2,D(A),nil,21,4.4 基于归结的问答系统,例：,已知：(,x)AT(John,x)AT(Fido,x),AT(John,School),求证：(x)AT(Fido,x),子句集：,AT(John,x,1,)AT(Fido,x,1,),AT(John,School),AT(Fido,x,2,),22,AT(Fido,x,2,),AT(John,x,1,),AT(Fido,x,1,),子句集：AT(John,x,1,)AT(Fido,x,1,),AT(John,School),AT(Fido,x,2,),AT(John,x,2,),x2/x1,AT(John,School),nil,School/x,2,AT(Fido,x,2,),AT(Fido,x,2,),AT(Fido,School),23,提取回答的过程,先进行归结，证明结论的正确性；,用重言式代替结论求反得到的子句；,按照证明过程，进行归结；,最后，在原来为空的地方，得到的就是提取的回答。,修改后的证明树称为,修改证明树,24,例：猴子摘香蕉问题,c,25,问题的表示,已知：,1,ON(s,0,),2,(,x)(s)(ON(s)AT(box,x,push(x,s),3,(s)(ON(climb(s),4,(s)(ON(s)AT(box,c,s)HB(grasp(s),5,(,x)(s)(AT(box,x,s)AT(box,x,climb(s),求解：(s)HB(s),26,问题的子句集,1,ON(s,0,),2,ON(s,1,)AT(box,x,1,push(x,1,s,1,),3,ON(climb(s,2,),4,ON(s,3,)AT(box,c,s,3,)HB(grasp(s,3,),5,AT(box,x,4,s,4,)AT(box,x,4,climb(s,4,),6,HB(s,5,),27,HB(s,5,),ON(s,3,)AT(box,c,s,3,)HB(grasp(s,3,),ON(s,3,)AT(box,c,s,3,),grasp(s,3,)/s,5,ON(climb(s,2,),climb(s,2,)/s,3,AT(box,c,climb(s,2,),ON(s,0,),ON(s,1,)AT(box,x,1,push(x,1,s,1,),s,0,/s,1,AT(box,x1,push(x1,s0),AT(box,x,4,s,4,)AT(box,x,4,climb(s,4,),x,4,/x,1,push(x,4,s,0,)/s,4,AT(box,x,4,climb(push(x,4,s,0,),NIL,c/x,4,push(c,s,0,)/s,2,HB(s,5,),HB(grasp(s,3,),HB(grasp(climb(s,2,),HB(grasp(climb(push(c,s,0,),1,ON(s,0,),2,ON(s,1,)AT(box,x,1,push(x,1,s,1,),3,ON(climb(s,2,),4,ON(s,3,)AT(box,c,s,3,)HB(grasp(s,3,),5,AT(box,x,4,s,4,)AT(box,x,4,climb(s,4,),6,HB(s,5,),28,归结方法小结,求子句集，进行归结，方法简单,通过修改证明树的方法，提取回答,方法通用,求解效率低，不宜引入启发信息,不宜理解推理过程,29,4.5 基于规则的正向演绎系统,问题：,归结方法不自然,可能会丢失蕴涵关系中所包含的控制信息,例：,以下蕴涵式：,A,B CC A B,A,C BA C B,B,C A B A C,均与子句(A B C),等价，但显然上面的蕴涵式信息更丰富。,30,事实表达式的与或形及其表达,与或形,无量词约束,否定符只作用于单个文字,只有“与”、“或”,例：,(u)(v)(Q(v,u)(R(v)P(v)S(u,v),=(u)(v)(Q(v,u)(R(v)P(v)S(u,v),=Q(v,A)(R(v)P(v)S(A,v),Skolem,化,=Q(,w,A)(R(v)P(v)S(A,v),主合取元变量换名,31,事实的与或树表示,例：,Q(w,A)(R(v)P(v)S(A,v),Q(w,A)(R(v)P(v)S(A,v),Q(w,A),(R(v)P(v)S(A,v),R(v)P(v),S(A,v),R(v),P(v),解图集：Q(w,A),R(v),S(A,v),P(v)S(A,v),32,应用规则对与或图作变换,对规则的形式：,L,W,其中，L是单文字，W是与或形，变量受全称量词约束,例：(x)(,(y)(z)P(x,y,z),(u)Q(x,u),=(x)(,(y)(z)P(x,y,z),(u)Q(x,u),=(x)(,(y)(z)P(x,y,z),(u)Q(x,u),=(x)(y)(z)(u)(P(x,y,z)Q(x,u),=P(x,y,f(x,y)Q(x,u),=P(x,y,f(x,y)Q(x,u),=P(x,1,y,1,f(x,1,y,1,)Q(x,1,u,1,),换名,例：(L,1,L,2,)W=L,1,W,和 L,2,W,33,命题逻辑的情况,例：,事实：(P,Q)R)(S (T U),规则：S (X Y)Z,34,(P,Q)R)(S (T U),(P,Q)R,S (T U),P,Q,R,S,T U,P,Q,T,U,S,X Y,Z,X,Y,P,Q S,P,Q T U,S R,R T U,P Q X Z,P Q Y Z,R X Z,R Y Z,规则的子句：,S (X Y)Z,=S,(X Y)Z,=,S,X Z,S,Y Z,结论：加入规则后得到的解图，是事实与规则对应子句的归结式,规则：,S (X Y)Z,35,例：,事实：A,B,规则集：,A C D,B E G,目标公式：,C G,A,B,A,B,A,C,D,B,E,G,C,G,目标,36,谓词逻辑的情况,事实表达式化成与或形,规则化成L,W,的形式，其中L为单文字,目标,用Skolem 化的,对偶形式,，即,消去全称量词，用Skolem函数代替,保留存在量词,对析取元作变量换名,例：(y)(x)(P(x,y)Q(x,y),=(y)(P(f(y),y)Q(f(y),y),=P(f(y,1,),y,1,)Q(f(y,2,),y,2,),换名,规则每使用一次，都要进行一次换名,37,例：事实：P(x,y),(Q(x,A)R(B,y),规则集：P(A,B)(S(A)X(B),Q(B,A)U(A),R(B,B)V(B),目标：S(A)X(B)U(A)V(B),P(x,y),(Q(x,A)R(B,y),P(x,y),Q(x,A)R(B,y),Q(x,A),R(B,y),P(A,B),A/x,B/y,S(A),X(B),Q(B,A),B/x,U(A),R(B,B),B/y,V(B),38,一致解图,如果一个解图中所涉及的置换是一致的，则该解图称为一致解图。,设有置换集u,1,u,2,u,n,其中:u,i,=t,i1,/v,i1,t,in,/v,in,，定义表达式：,U,1,=(v,1,1,v,1,m1,v,n,1,v,n,mn,),U,2,=(t,1,1,t,1,m1,t,n,1,t,n,mn,),置换集u,1,u,2,u,n,称为一致的，当且仅当U,1,和U,2,是可合一的。U,1,、U,2,的mgu是u,1,u,2,u,n,的合一复合。,置换集的合一复合运算是可结合和可交换的。,39,一致置换举例,40,举例,事实：,D(F),(B(F)I(F),规则：,R,1,:D(x)T(x),R,2,:B(y)N(y),目标：,T(u)N(v),41,D(F),(B(F)I(F),D(F),B(F)I(F),B(F),I(F),D(x),F/x,T(F),R,1,T(u),F/u,B(y),F/y,N(F),R,2,N(v),F/v,目标,目标,U,1,=(x,u,y,v),U,2,=(F,F,F,F),合一复合u：,F/x,F/u,F/y,F/v,作用于目标：,T(u),N(v),u,=T(F)N(F),规则：,R,1,:D(x)T(x),R,2,:B(y)N(y),目标：,T(u)N(v),42,正向演绎系统小结,事实表达式为与或形,规则形式：L,W,其中L为单文字,目标公式为文字析取,对事实和规则进行Skolem化，消去存在量词，变量受全称量词约束，对,主合取元,和,规则,中的,变量换名,用“,对偶形,”对目标进行Skolem化，消去全称量词，变量受存在量词约束，对,析取元,中的,变量换名,事实表达成与或树，其中，“,”对应树中“,与,”，“,”对应树中“,或,”,从事实出发，,正向,应用规则，到得到目标节点为结束的,一致解图,为止,存在合一复合时，则解图是一致的,43,4.6 基于规则的逆向演绎系统,目标为任意形的表达式,用“,对偶形,”对目标进行Skolem化，即消去全称量词，变量受存在量词约束，对主,析取,元中的变量换名,目标用与或树表示，,其中，“,”对应树中“,与,”，“,”对应树中“,或,”,事实表达式是文字的,合取,规则形式：L,W,其中W为单文字，如形为：,L,W,1,W,2,，则变换为：,L,W,1,和,L,W,2,从,目标,出发，,逆向,应用规则，到得到事实节点为结束条件的一致解图为止,44,例：,事实：D(F),B(F),W(F),M(N),规则：,R,1,:(W(x,1,),D(x,1,),F(x,1,),R,2,:(F(x,2,)B(x,2,),A(y,2,x,2,),R,3,:D(x,3,)A(x,3,),R,4,:C(x,4,)A(x,4,),R,5,:M(x,5,)C(x,5,),目标：,C(x)D(y)A(x,y),C(x)D(y)A(x,y),C(x),D(y),A(x,y),C(x,5,),x/x,5,M(x),R,5,M(N),N/x,D(F),F/y,A(y,2,x,2,),x/y,2,y/x,2,F(y),B(y),R,2,B(F),F/y,F(x,1,),y/x,1,W(y),D(y),R,1,W(F),F/y,D(F),F/y,45,一致性检查,置换集,x/x,5,N/x,F/y,x/y,2,y/x,2,F/y,y/x,1,F/y,F/y,U,1,=(x,5,x,y,y,2,x,2,y,x,1,y,y),U,2,=(x,N,F,x,y,F,y,F,F),合一复合,N/x,5,N/x,F/y,N/y,2,F/x,2,F/x,1,目标得到的解答,C(x)D(y)A(x,y),=C(N)D(F)A(N,F),46,Horn子句与PROLOG,Horn子句是一类特殊的子句，体现为下列三种形式：,规则：前项是正文字的合取，后项是单个正文字,事实：当前项为空时，表示事实,目标：当后项为空时，表示目标,Horn子句构成了PROLOG语言的基础,47,在PROLOG中的表示,规则：,P,n,:-P,n1,P,n2,P,nm,含义：P,n1,P,n2,P,nm,P,n,事实：,P,i,:-,目标：,:-P,j1,P,j2,P,jk,48,PROLOG,增加了“否定”，但不是真正意义下的否定,在规则前项中可以使用“或”，只是为了书写更方便。,采用回溯式搜索策略,PROLOG实际是一个基于规则的逆向系统,49,举例,1,On(a,b):-,2,On(b,c):-,3,Above(X,3,Y,3,):-On(X,3,Y,3,),4,Above(X,4,Y,4,):-On(X,4,Z,4,),Above(Z,4,Y,4,),目标：,:-Above(a,c),50,1,On(A,B):-,2,On(B,C):-,3,Above(x,3,y,3,):-On(x,3,y,3,),4,Above(x4,y4):-On(x4,z,4,),Above(z,4,y,4,),:-Above(A,C),Above(A,C),Above(x,3,y,3,),On(A,C),A/x,3,C/y,3,R,3,无匹配,Above(x,4,y,4,),On(A,z,4,),Above(z,4,C),A/x,4,C/y,4,R,4,On(A,B),B/z,4,事实1,B/z4,Above(x,3,y,3,),B/x,3,C/y,3,On(B,C),事实2,R,3,一致解图,51,4.7 一些深入的问题,修剪不一致的局部解图,建立规则连接图结构,规则的多次调用,规则的递归调用,加快匹配的速度,52,4.8 正、逆向系统对比,事实表达式任意形,规则形式：单文字,W,目标公式为文字析取,对事实、规则消存在量词，Skolem化,用对偶形消目标的全称量词，Skolem化,事实表达式与或树,，“,”对“与”，“”对应“或”,从事实出发，正向应用规则,以目标为结束的一致解图,事实表达式是合取形,规则形式：L,单文字,目标公式任意形,对事实、规则消存在量词，Skolem化,用对偶形消目标的全称量词，Skolem化,目标公式的与或树,，“,”对“与”，“”对应“或”,从目标出发，逆向应用规则,以事实为结束的一致解图,53,