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

1,第四章谓词演算及应用,是一种形式语言，具有严密的理论体系是一种常用的知识表示方法例：City（北京）City（上海）Age（张三，23）(x)(y)(z)(F(x,y)F(y,z)GF(x,z),2,4.1归结原理,归结原理是一种定理证明方法，1965年由Robinson提出，从理论上解决了定理证明问题。归结原理的提出，对机器定理证明问题起到了推动作用。,3,子句集,无量词约束元素只是文字的析取否定符只作用于单个文字元素间默认为合取例：I(z)R(z),I(A),R(x)L(x),D(y),4,化子句集的方法,例：(z)(x)(y)(P(x)Q(x)R(y)U(z)1,消蕴涵符理论根据：ab=ab(z)(x)(y)(P(x)Q(x)R(y)U(z)2,移动否定符理论根据：(ab)=ab(ab)=ab(x)P(x)=(x)P(x)(x)P(x)=(x)P(x)(z)(x)(y)(P(x)Q(x)R(y)U(z),5,化子句集的方法（续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),6,化子句集的方法（续2）,6,化为合取范式即(ab)(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),7,化子句集的方法（续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),8,归结原理,定理：若S是合式公式F的子句集，则F永假的充要条件是S不可满足。S不可满足：若nilS，则S不可满足。,9,使用归结原理证明定理的思路,目标的否定连同已知条件一起，化为子句集，并给出一种变换的方法，使得SS1S2.Sn同时保证当Sn不可满足时，有S不可满足。,10,4.2归结方法（命题逻辑）,设子句：C1=LC1C2=(L)C2则归结式C为：C=C1C2定理：子句集S=C1,C2,Cn与子句集S1=C,C1,C2,Cn的不可满足性是等价的。其中，C是C1和C2的归结式。,11,归结的例子,设公理集：P,(PQ)R,(ST)Q,T求证：R子句集：(1)P(2)PQR(3)SQ(4)TQ(5)T(6)R（目标求反）,化子句集：(PQ)R=(PQ)R=PQR(ST)Q=(ST)Q=(ST)Q=(SQ)(TQ)=SQ,TQ,12,子句集：(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),13,4.3谓词逻辑的归结原理,问题：如何找归结对例：P(x)Q(y),P(f(y)R(y)P(A)Q(y),P(f(y)R(y)基本概念置换s=t1/v1,t2/v2,tn/vn对公式E实施置换s后得到的公式称为E的例，记作Es。例：s1=z/x,A/y,则：Px,f(y),Bs=Pz,f(A),B,14,合一如果存在一个S置换，使得Ei中E1s=E2s=E3s=Ens，则称Ei是可合一的。S为Ei的合一者。例：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也都是这两个谓词公式的合一者。结论：合一者不唯一。,15,最一般合一者（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也不是唯一的。,16,合一算法,例：P(x,x,z),P(f(y),f(B),y)前缀表示：(Pxxz)(P(fy)(fB)y)置换：(fy)/x(P(fy)(fy)z)(P(fy)(fB)y)置换：B/y,并使得(fB)/x(P(fB)(fB)z)(P(fB)(fB)B)置换：B/z得到置换：(fB)/x，B/y，B/z置换后的结果：(P(fB)(fB)B),17,谓词逻辑的归结方法,对于子句C1L1和C2L2，如果L1与L2可合一，且s是其合一者，则(C1C2)s是其归结式。例：P(x)Q(y),P(f(z)R(z)=Q(y)R(z),18,归结举例,设公理集：(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),19,(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),20,目标求反：(x)(I(x)R(x)=(x)(I(x)R(x)=(x)(I(x)R(x)=I(x)R(x)(5)换名后得字句集：R(x1)L(x1)D(x2)L(x2)D(A)I(A)I(x5)R(x5),21,例题的归结树,R(x1)L(x1)D(x2)L(x2)D(A)I(A)I(x5)R(x5),I(A),I(x5)R(x5),R(A),A/x5,R(x1)L(x1),L(A),A/x1,D(x2)L(x2),D(A),A/x2,D(A),nil,22,4.4基于归结的问答系统,例：已知：(x)AT(John,x)AT(Fido,x)AT(John,School)求证：(x)AT(Fido,x)子句集：AT(John,x1)AT(Fido,x1)AT(John,School)AT(Fido,x2),23,AT(Fido,x2),AT(John,x1)AT(Fido,x1),子句集：AT(John,x1)AT(Fido,x1)AT(John,School)AT(Fido,x2),x2/x1,AT(John,School),School/x2,AT(Fido,x2),AT(Fido,x2),AT(Fido,School),24,提取回答的过程,先进行归结，证明结论的正确性；用重言式代替结论求反得到的子句；按照证明过程，进行归结；最后，在原来为空的地方，得到的就是提取的回答。修改后的证明树称为修改证明树,25,例：猴子摘香蕉问题,26,问题的表示,已知：1,ON(s0)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),27,问题的子句集,1,ON(s0)2,ON(s1)AT(box,x1,push(x1,s1)3,ON(climb(s2)4,ON(s3)AT(box,c,s3)HB(grasp(s3)5,AT(box,x4,s4)AT(box,x4,climb(s4)6,HB(s5),28,HB(s5),ON(s3)AT(box,c,s3)HB(grasp(s3),ON(s3)AT(box,c,s3),grasp(s3)/s5,ON(climb(s2),climb(s2)/s3,AT(box,c,climb(s2),ON(s0),ON(s1)AT(box,x1,push(x1,s1),s0/s1,AT(box,x1,push(x1,s0),AT(box,x4,s4)AT(box,x4,climb(s4),x4/x1,push(x4,s0)/s4,AT(box,x4,climb(push(x4,s0),NIL,c/x4,push(c,s0)/s2,HB(s5),HB(grasp(s3),HB(grasp(climb(s2),HB(grasp(climb(push(c,s0),1,ON(s0)2,ON(s1)AT(box,x1,push(x1,s1)3,ON(climb(s2)4,ON(s3)AT(box,c,s3)HB(grasp(s3)5,AT(box,x4,s4)AT(box,x4,climb(s4)6,HB(s5),29,归结方法小结,求子句集，进行归结，方法简单通过修改证明树的方法，提取回答方法通用求解效率低，不宜引入启发信息不宜理解推理过程,30,4.5基于规则的正向演绎系统,问题：归结方法不自然可能会丢失蕴涵关系中所包含的控制信息例：以下蕴涵式：ABCCABACBACBBCABAC均与子句(ABC)等价，但显然上面的蕴涵式信息更丰富。,31,事实表达式的与或形及其表达,与或形无量词约束否定符只作用于单个文字只有“与”、“或”例：(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)主合取元变量换名,32,事实的与或树表示,例：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),33,应用规则对与或图作变换,对规则的形式：LW其中，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(x1,y1,f(x1,y1)Q(x1,u1)换名例：(L1L2)W=L1W和L2W,34,命题逻辑的情况,例：事实：(PQ)R)(S(TU)规则：S(XY)Z,35,(PQ)R)(S(TU),(PQ)R,S(TU),PQ,R,S,TU,P,Q,T,U,S,XY,Z,X,Y,PQSPQTUSRRTUPQXZPQYZRXZRYZ,规则的子句：S(XY)Z=S(XY)Z=SXZSYZ,结论：加入规则后得到的解图，是事实与规则对应子句的归结式,规则：S(XY)Z,36,例：事实：AB规则集：ACDBEG目标公式：CG,AB,A,B,A,C,D,B,E,G,C,G,目标,37,谓词逻辑的情况,事实表达式化成与或形规则化成LW的形式，其中L为单文字目标用Skolem化的对偶形式，即消去全称量词，用Skolem函数代替保留存在量词对析取元作变量换名例：(y)(x)(P(x,y)Q(x,y)=(y)(P(f(y),y)Q(f(y),y)=P(f(y1),y1)Q(f(y2),y2)换名规则每使用一次，都要进行一次换名,38,例：事实：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),39,一致解图,如果一个解图中所涉及的置换是一致的，则该解图称为一致解图。设有置换集u1,u2,un,其中:ui=ti1/vi1,tin/vin，定义表达式：U1=(v1,1,v1,m1,vn,1,vn,mn)U2=(t1,1,t1,m1,tn,1,tn,mn)置换集u1,u2,un称为一致的，当且仅当U1和U2是可合一的。U1、U2的mgu是u1,u2,un的合一复合。置换集的合一复合运算是可结合和可交换的。,40,一致置换举例,41,举例,事实：D(F)(B(F)I(F)规则：R1:D(x)T(x)R2:B(y)N(y)目标：T(u)N(v),42,D(F)(B(F)I(F),D(F),B(F)I(F),B(F),I(F),D(x),F/x,T(F),R1,T(u),F/u,B(y),F/y,N(F),R2,N(v),F/v,目标,目标,U1=(x,u,y,v)U2=(F,F,F,F)合一复合u：F/x,F/u,F/y,F/v作用于目标：T(u)N(v)u=T(F)N(F),规则：R1:D(x)T(x)R2:B(y)N(y)目标：T(u)N(v),43,正向演绎系统小结,事实表达式为与或形规则形式：LW,其中L为单文字目标公式为文字析取对事实和规则进行Skolem化，消去存在量词，变量受全称量词约束，对主合取元和规则中的变量换名用“对偶形”对目标进行Skolem化，消去全称量词，变量受存在量词约束，对析取元中的变量换名事实表达成与或树，其中，“”对应树中“与”，“”对应树中“或”从事实出发，正向应用规则，到得到目标节点为结束的一致解图为止存在合一复合时，则解图是一致的,44,4.6基于规则的逆向演绎系统,目标为任意形的表达式用“对偶形”对目标进行Skolem化，即消去全称量词，变量受存在量词约束，对主析取元中的变量换名目标用与或树表示，其中，“”对应树中“与”，“”对应树中“或”事实表达式是文字的合取规则形式：LW,其中W为单文字，如形为：LW1W2，则变换为：LW1和LW2从目标出发，逆向应用规则，到得到事实节点为结束条件的一致解图为止,45,例：事实：D(F)B(F)W(F)M(N)规则：R1:(W(x1)D(x1)F(x1)R2:(F(x2)B(x2)A(y2,x2)R3:D(x3)A(x3)R4:C(x4)A(x4)R5:M(x5)C(x5)目标：C(x)D(y)A(x,y),C(x)D(y)A(x,y),C(x),D(y),A(x,y),C(x5),x/x5,M(x),R5,M(N),N/x,D(F),F/y,A(y2,x2),x/y2,y/x2,F(y),B(y),R2,B(F),F/y,F(x1),y/x1,W(y),D(y),R1,W(F),F/y,D(F),F/y,46,一致性检查,置换集x/x5,N/x,F/y,x/y2,y/x2,F/y,y/x1,F/y,F/yU1=(x5,x,y,y2,x2,y,x1,y,y)U2=(x,N,F,x,y,F,y,F,F)合一复合N/x5,N/x,F/y,N/y2,F/x2,F/x1目标得到的解答C(x)D(y)A(x,y)=C(N)D(F)A(N,F),47,Horn子句与PROLOG,Horn子句是一类特殊的子句，体现为下列三种形式：规则：前项是正文字的合取，后项是单个正文字事实：当前项为空时，表示事实目标：当后项为空时，表示目标Horn子句构成了PROLOG语言的基础,48,在PROLOG中的表示,规则：Pn:-Pn1,Pn2,Pnm含义：Pn1Pn2PnmPn事实：Pi:-目标：:-Pj1,Pj2,Pjk,49,PROLOG,增加了“