人工智能導論：第五章 謂詞演算及應用

1第五章謂詞演算及應用是一種形式語言，具有嚴密的理論體系是一種常用的知識表示方法例：City（北京）City（上海）Age（張三，23）(x)(y)(z)(F(x,y)F(y,z)GF(x,z)25.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,消蘊涵符 理論根據(jù)：ab=>~ab (z)(x)(y){[~(P(x)Q(x))R(y)]U(z)}2,移動否定符 理論根據(jù)：~(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)}5化子句集的方法（續(xù)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化） 原則：對于一個受存在量詞約束的變量，如果他不受全程量詞約束，則該變量用一個常量代替，如果他受全程量詞約束，則該變量用一個函數(shù)代替。

(z)(x)(y){[(~P(x)~Q(x))R(y)]U(z)}=>(x){[(~P(x)~Q(x))R(f(x))]U(a)}6化子句集的方法（續(xù)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化子句集的方法（續(xù)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使用歸結原理證明定理的思路

目標的否定連同已知條件一起，化為子句集，并給出一種變換的方法，使得S

S1S2...Sn同時保證當Sn不可滿足時，有S不可滿足。105.2歸結方法（命題邏輯）設子句： C1=LC1’ C2=(~L)C2’ 則歸結式C為： C=C1’C2’定理： 子句集S={C1,C2,…,Cn}與子句集 S1={C,C1,C2,…,Cn}的不可滿足性是等價的。其中，C是C1和C2的歸結式。11歸結的例子設公理集：

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}12子句集：

(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)135.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。例：s={z/x,A/y},則：

P[x,f(y),B]s=P[z,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)nil225.4基于歸結的問答系統(tǒng)例：已知：(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)~AT(John,x2){x2/x1}AT(John,School)nil{School/x2}AT(Fido,x2)AT(Fido,x2)AT(Fido,School)24提取回答的過程先進行歸結，證明結論的正確性；用重言式代替結論求反得到的子句；按照證明過程，進行歸結；最后，在原來為空的地方，得到的就是提取的回答。修改后的證明樹稱為修改證明樹25例：猴子摘香蕉問題c26問題的表示已知：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歸結方法小結求子句集，進行歸結，方法簡單通過修改證明樹的方法，提取回答方法通用求解效率低，不宜引入啟發(fā)信息不宜理解推理過程5.5基于規(guī)則的逆向演繹系統(tǒng)問題：歸結方法不自然可能會丟失蘊涵關系中所包含的控制信息例：

以下蘊涵式：

~A~BC ~CAB

~A~CB ~ACB

~B~CA ~BAC

均與子句(ABC)等價，但顯然上面的蘊涵式信息更豐富。30形式上的要求目標為任意表達式事實表達式是文字的合取規(guī)則形式：LW,其中W為單文字，如形為：LW1W2，則變換為： LW1

和LW2

變量收全稱量詞約束對目標逆向使用規(guī)則31目標用Skolem化的對偶形式，即消去全稱量詞，用Skolem函數(shù)代替保留存在量詞對主析取元作變量換名例：(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) 換名32對目標表達式的處理目標的與或樹表示33例：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)34對規(guī)則的處理對規(guī)則的形式：LW其中，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) 換名應用規(guī)則對與或圖做變換35例：目標：Q(w,A)((~R(v)~P(v))~S(A,v))規(guī)則：

P(u)Q(v,A)~S(u,B)假設w,u,v是變量，A、B是常量36Q(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)~S(u,B){A/u,B/v}P(A)Q(B,A)37一致解圖如果一個解圖中所涉及的置換是一致的，則該解圖稱為一致解圖。設有置換集{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}的合一復合。置換集的合一復合運算是可結合和可交換的。38一致置換舉例39例：事實：D(F)~B(F)W(F)M(N)規(guī)則：

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)R5M(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)R1W(F){F/y}D(F){F/y}40一致性檢查置換集

{{x/x5},{N/x},{F/y},{x/y2,y/x2},{F/y},{y/x1},{F/y},{F/y}} U1=(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)41Horn子句與PROLOG程序設計語言的類型過程型，函數(shù)型，邏輯型，面向對象…PROLOG語言PROgramminginLOGic1972年誕生與法國的馬賽大