精品大学课件-人工智能导论-马少平(清华)-人工智能

第四章谓词演算及应用是一种形式语言，具有严密的理论体系是一种常用的知识表示方法例：City〔北京〕City〔上海〕Age〔张三，23〕(x)(y)(z)(F(x,y)F(y,z)GF(x,z)4.1归结原理归结原理是一种定理证明方法，1965年由Robinson提出，从理论上解决了定理证明问题。子句集词约束元素只是文字的析取否认符只作用于单个文字元素间默认为和取例：{~I(z)R(z),I(A),~R(x)L(x),~D(y)}化子句集的方法例：(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)=>~a~b ~(ab)=>~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)}化子句集的方法〔续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)}化子句集的方法〔续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)]}化子句集的方法〔续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)}定理： 假设S是合式公式F的子句集，那么F永假的充要条件是S不可满足。S不可满足：假设nilS，那么S不可满足。证明的思路： 目标的否认连同条件一起，化为子句集，并给出一种变换的方法，使得 S

S1S2...Sn

同时保证当Sn不可满足时，有S不可满足。

4.2归结方法〔命题逻辑〕设子句： C1=LC1’ C2=(~L)C2’ 那么归结式C为： C=C1’C2’定理： 子句集S={C1,C2,…,Cn}与子句集 S1={C,C1,C2,…,Cn}的不可满足性是等价的。其中，C是C1和C2的归结式。归结的例子设公理集： P, (PQ)R, (ST)Q, T求证：R子句集： (1)P (2)~P~QR (3)~SQ (4)~TQ (5)T (6)~R〔目标求反〕

化子句集： (PQ)R=>~(PQ)R=>~P~QR (ST)Q=>~(ST)Q=>(~S~T)Q=>(~SQ)(~TQ)=>{~SQ,~TQ}子句集： (1)P (2)~P~QR (3)~SQ (4)~TQ (5)T (6)~R〔目标求反〕归结： (7)~P~Q(2,6) (8)~Q (1,7)(9)~T(4,8)(10)nil(5,9)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,Ay},那么： P[x,f(y),B]s=P[z,f(A),B]合一 如果存在一个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}也都是合一者。结论：合一者不唯一。最一般合一者〔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也不是唯一的。合一算法例：{P(x,x,B),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)谓词逻辑的归结方法对于子句C1L1和C2L2，如果L1与~L2可合一，且s是其合一者，那么(C1C2)s是其归结式。例：P(x)Q(y),~P(f(z))R(z) =>Q(y)R(z)归结举例设公理集： (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) (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)目标求反： ~(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)例题得归结树 ~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)nil4.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)~AT(Fido,x2)~AT(John,x1)AT(Fido,x1)子句集： ~AT(John,x1)AT(Fido,x1) AT(John,School) ~AT(Fido,x2)~AT(John,x2){x2/x1}AT(John,School)nil{School/x2}AT(Fido,x2)AT(Fido,x2)AT(Fido,School)提取答复的过程先进行归结，证明结论的正确性；用重言式代替结论求反得到的子句；按照证明过程，进行归结；最后，在原来为空的地方，得到的就是提取的答复。修改后的证明树称为修改证明树例：猴子摘香蕉问题c问题的表示：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)问题的子句集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)返回~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))))归结方法小结求子句集，进行归结，方法简单通过修改证明树的方法，提取答复方法通用求解效率低，不宜引入启发信息不宜理解推理过程4.5基于规那么的正向演绎系统问题：归结方法不自然可能会丧失蕴涵关系中所包含的控制信息例：

以下蕴涵式：

~A~BC ~CAB

~A~CB ~ACB

~B~CA ~BAC

均与子句(ABC)等价，但显然上面的蕴涵式信息更丰富。事实表达式的与或形及其表达与或形词约束否认符只作用于单个文字只有“与〞、“或〞例： (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))

主合取元变量换名事实的与或树表示例：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)应用规那么对与或图作变换对规那么的形式：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命题逻辑的情况例：

事实：((PQ)R)(S(TU)) 规那么：S(XY)Z((PQ)R)(S(TU))(PQ)RS(TU)PQRSTUPQTUSXYZXYPQSPQTUSRRTUPQXZPQYZRXZRYZ规那么的子句：S(XY)Z=>~S(XY)Z=>~SXZ

~SYZ结论：参加规那么后得到的解图，是事实与规那么对应子句的归结式例：事实：AB规那么集：ACDBEG目标公式：CGABABACDBEGCG目标谓词逻辑的情况事实表达式化成与或形规那么化成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) 换名规那么每使用一次，都要进行一次换名例：事实：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)一致解图如果一个解图中所涉及的置换是一致的，那么该解图称为一致解图。设有置换集{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}的合一复合。置换集的合一复合运算是可结合和可交换的。一致置换举例举例事实： ~D(F)(B(F)I(F))规那么： R1:~D(x)~T(x) R2:B(y)N(y)目标： ~T(u)N(v)~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)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)正向演绎系统小结事实表达式为与或形规那么形式：LW,其中L为单文字目标公式为文字析取对事实和规那么进行Skolem化，消去存在量词，变量受全称量词约束，对主合取元和规那么中的变量换名用“对偶形〞对目标进行Skolem化，消去全称量词，变量受存在量词约束，对析取元中的变量换名事实表达成与或树，其中，“〞对应树中“与〞，“〞对应树中“或〞从事实出发，正向应用规那么，到得到目标节点为结束的一致解图为止存在合一复合时，那么解图是一致的4.6基于规那么的逆向演绎系统目标为任意形的表达式用“对偶形〞对目标进行Skolem化，即消去全称量词，变量受存在量词约束，对主析取元中的变量换名目标用与或树表示，其中，“〞对应树中“与〞，“〞对应树中“或〞事实表达式是文字的合取规那么形式：LW,其中W为单文字，如形为： LW1W2，那么变换为： LW1和LW2从目标出发，逆向应用规那么，到得到事实节点为结束条件的一致解图为止例：事实：D(F)~B(F)W(F)M(N)规那么：