1、1l是一种形式语言，具有严密的理论体系l是一种常用的知识表示方法例：City（北京）City（上海）Age（张三，23）(x)(y)(z)(F(x,y)F(y,z)GF(x,z)2l归结原理是一种定理证明方法，1965年由Robinson提出，从理论上解决了定理证明问题。l归结原理的提出，对机器定理证明问题起到了推动作用。3l无量词约束l元素只是文字的析取l否定符只作用于单个文字l元素间默认为合取l例：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,消蕴涵符理论根据：a b=a b(z)(x)(y)(P(x)Q(x)R(y)U
2、(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)53,变量标准化即：对于不同的约束，对应于不同的变量(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)
3、R(f(x)U(a)66,化为合取范式即(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)78,表示为子句集 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目标的否定连同已知条件一
4、起，化为子句集，并给出一种变换的方法，使得 S S1 S2.Sn同时保证当Sn不可满足时，有S不可满足。10l设子句：C1=LC1C2=(L)C2则归结式C为：C=C1 C2l定理：子句集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,TQ12子句集：(1)P(2)PQR(3)SQ(4)TQ(5)T(6)R（目
5、标求反）归结：(7)PQ (2,6)(8)Q (1,7)(9)T (4,8)(10)nil (5,9)13l问题：如何找归结对例：P(x)Q(y),P(f(y)R(y)P(A)Q(y),P(f(y)R(y)l基本概念置换s=t1/v1,t2/v2,tn/vn对公式E实施置换s后得到的公式称为E的例，记作Es。例：s1=z/x,A/y,则：Px,f(y),Bs=Pz,f(A),B14l合一如果存在一个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,
6、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也都是这两个谓词公式的合一者。结论：合一者不唯一。15l最一般合一者（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)lmgu也不是唯一的。16例：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
7、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)17l对于子句C1L1和C2L2，如果L1与L2可合一，且s是其合一者，则(C1C2)s是其归结式。l例：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
8、)(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)20l目标求反：(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)21R(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)nil22l例：已知：(x)AT(Joh
9、n,x)AT(Fido,x)AT(John,School)求证：(x)AT(Fido,x)子句集：AT(John,x1)AT(Fido,x1)AT(John,School)AT(Fido,x2)23AT(Fido,x2)AT(John,x1)AT(Fido,x1)子句集：AT(John,x1)AT(Fido,x1)AT(John,School)AT(Fido,x2)AT(John,x2)x2/x1AT(John,School)nilSchool/x2AT(Fido,x2)AT(Fido,x2)AT(Fido,School)24l先进行归结，证明结论的正确性；l用重言式代替结论求反得到的子句；l
10、按照证明过程，进行归结；l最后，在原来为空的地方，得到的就是提取的回答。l修改后的证明树称为修改证明树25c26已知：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)271,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(
11、box,x4,climb(s4)6,HB(s5)28HB(s5)ON(s3)AT(box,c,s3)HB(grasp(s3)ON(s3)AT(box,c,s3)grasp(s3)/s5ON(climb(s2)climb(s2)/s3 AT(box,c,climb(s2)ON(s0)ON(s1)AT(box,x1,push(x1,s1)s0/s1AT(box,x1,push(x1,s0)AT(box,x4,s4)AT(box,x4,climb(s4)x4/x1,push(x4,s0)/s4AT(box,x4,climb(push(x4,s0)NILc/x4,push(c,s0)/s2HB(s5)
12、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)29l求子句集，进行归结，方法简单l通过修改证明树的方法，提取回答l方法通用l求解效率低，不易引入启发信息l不易理解推理过程30l问题：归结方法不自然可能会丢失蕴涵关系中所包含的控制信息l例：以下蕴涵式：A B CC A BA C BA C
13、 BB C A B A C均与子句(A B C)等价，但显然上面的蕴涵式信息更丰富。31l与或形无量词约束否定符只作用于单个文字只有“与”、“或”l例：(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,
14、v),P(v)S(A,v)33l对规则的形式：L W其中，L是单文字，W是与或形，变量受全称量词约束l例：(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)换名l例：(L1 L2)W=L1 W 和 L2 W 34l例：事实：(P Q)R)(S (T U)规则：S (X Y)Z 35(P Q)R)(S (T
15、U)(P Q)R S (T U)P Q R ST UPQTUSX YZX YP Q SP Q T US RR T UP Q X ZP Q Y ZR X ZR Y Z规则的子句：S (X Y)Z=S(X Y)Z=S X Z S Y Z结论：加入规则后得到的解图，是事实与规则对应子句的归结式规则：S (X Y)Z36例：事实：A B规则集：A C D B E G目标公式：C GA BABACDBEGCG目标37l事实表达式化成与或形l规则化成L W的形式，其中L为单文字l目标目标用Skolem 化的对偶形式对偶形式，即消去全称量词，用Skolem函数代替保留存在量词对析取元作变量换名例：(y)(x
16、)(P(x,y)Q(x,y)=(y)(P(f(y),y)Q(f(y),y)=P(f(y1),y1)Q(f(y2),y2)换名l规则每使用一次，都要进行一次换名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/yS(A)X(B)Q(B,A)B/xU(A)R(B,B)B/yV(B)39l如果一个解图中所涉及的置换是一致的，则该解图称为一致解图。l设有置换集u1,
17、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的合一复合。l置换集的合一复合运算是可结合和可交换的。40u1 u2 U1和 U2 合一复合 A/x B/x U1=(x,x)U2=(A,B)不一致 x/y y/z U1=(y,z)U2=(x,y)x/y,x/z f(z)/x f(A)/x U1=(x,x)U2=(f(z),f(A)f(A)/x,A/z x/y,x/z A/z
18、 U1=(y,z,z)U2=(x,x,A)A/x,A/y,A/z 41事实：D(F)(B(F)I(F)规则：R1:D(x)T(x)R2:B(y)N(y)目标：T(u)N(v)42D(F)(B(F)I(F)D(F)B(F)I(F)B(F)I(F)D(x)F/xT(F)R1T(u)F/uB(y)F/yN(F)R2N(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)43l事实表达式为与或形l规则形式：L W,其中L为单文字
19、l目标公式为文字析取l对事实和规则进行Skolem化，消去存在量词，变量受全称量词约束，对主合取元和规则中的变量换名l用“对偶形”对目标进行Skolem化，消去全称量词，变量受存在量词约束，对析取元中的变量换名l事实表达成与或树，其中，“”对应树中“与”，“”对应树中“或”l从事实出发，正向应用规则，到得到目标节点为结束的一致解图为止l存在合一复合时，则解图是一致的44l目标为任意形的表达式l用“对偶形”对目标进行Skolem化，即消去全称量词，变量受存在量词约束，对主析取元中的变量换名l目标用与或树表示，其中，“”对应树中“与”，“”对应树中“或”l事实表达式是文字的合取l规则形式：L W,
20、其中W为单文字，如形为：L W1 W2，则变换为：L W1 和 L W2l从目标出发，逆向应用规则，到得到事实节点为结束条件的一致解图为止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/x5M(x)R5M(N)N/xD(F)F/yA(y2,x2)x/y2,y/x2F(y)B(y)R2B(F)F/yF(x1)y/x1W(y)D(y)
21、R1W(F)F/yD(F)F/y46l置换集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)l合一复合N/x5,N/x,F/y,N/y2,F/x2,F/x1l目标得到的解答 C(x)D(y)A(x,y)=C(N)D(F)A(N,F)47lHorn子句是一类特殊的子句，体现为下列三种形式：规则：前项是正文字的合取，后项是单个正文字事实：当前项为空时，表示事实目标：当后项为空时，表示目标lHorn子句构成了PROLOG语言的基础48l规则：Pn:-Pn1,Pn2,Pnm含义
22、：Pn1Pn2Pnm Pnl事实：Pi:-l目标：:-Pj1,Pj2,Pjk49l增加了“否定”，但不是真正意义下的否定l在规则前项中可以使用“或”，只是为了书写更方便。l采用回溯式搜索策略lPROLOG实际是一个基于规则的逆向系统501,On(a,b):-2,On(b,c):-3,Above(X3,Y3):-On(X3,Y3)4,Above(X4,Y4):-On(X4,Z4),Above(Z4,Y4)目标：:-Above(a,c)511,On(A,B):-2,On(B,C):-3,Above(x3,y3):-On(x3,y3)4,Above(x4,y4):-On(x4,z4),Above(z
23、4,y4):-Above(A,C)Above(A,C)Above(x3,y3)On(A,C)A/x3,C/y3R3无匹配Above(x4,y4)On(A,z4)Above(z4,C)A/x4,C/y4R4On(A,B)B/z4事实1B/z4Above(x3,y3)B/x3,C/y3On(B,C)事实2R3一致解图52l修剪不一致的局部解图l建立规则连接图结构l规则的多次调用l规则的递归调用l加快匹配的速度53l事实表达式任意形l规则形式：单文字 Wl目标公式为文字析取l对事实、规则消存在量词，Skolem化l用对偶形消目标的全称量词，Skolem化l事实表达式与或树，“”对“与”，“”对应“或”l从事实出发，正向应用规则l以目标为结束的一致解图l事实表达式是合取形l规则形式：L 单文字l目标公式任意形l对事实、规则消存在量词，Skolem化l用对偶形消目标的全称量词，Skolem化l目标公式的与或树，“”对“与”，“”对应“或”l从目标出发，逆向应用规则l以事实为结束的一致解图
