吉林大學(xué)研究生人工智能t演示文檔
.,6/27/2018,1,第六章 歸結(jié)原理,6.1 子句集的Herbrand域 一、 Herbrand域與 Herbrand解釋定義(Herbrand域)設(shè)S為子句集,令H0是出現(xiàn)于子句集S的常量符號集。如果S中無常量符號出現(xiàn),則H0由一個常量符號a組成。 對于i1,2,令 Hi = Hi-1所有形如f(t1,tn)的項 其中f(t1,tn)是出現(xiàn)在S中的所有n元函數(shù)符號, tj Hi-1,j1,n 稱Hi為S的i級常量集,H 稱為S的Herbrand域, 簡稱S的H域。,.,6/27/2018,2,例 SP(f(x),a,g(y),b) H0 =a, b H1 =a, b, f(a), f(b), g(a), g(b) H2a, b, f(a), f(b), g(a), g(b), f(f(a), f(f(b), f(g(a), f(g(b), g(f(a), g(f(b), g(g(a), g(g(b) ,.,6/27/2018,3,練習(xí): 求S的Herbrand域,SP(x) Q(y),R(z) SQ(a) P(f(x), Q(b) P(g(x,y) ,.,6/27/2018,4,原子集 基例,基:把對象中的變量用常量代替后得到的無變量符號出現(xiàn)的對象。 基項、基項集、基原子、基原子集合、基文字、基子句、基子句集 定義 (原子集、Herbrand底) 設(shè)S是子句集,形如P(t1,tn)的基原子集合,稱為S的Herbrand底或S的原子集 其中P(x1,xn)是出現(xiàn)于S的所有n元謂詞符號,t1,tn是S的H域中的元素定義(基例) 設(shè)S是子句集,C是S中的一個子句用S的H域中元素代替C中所有變量所得到的基子句稱為子句C的基例。,.,6/27/2018,5,練習(xí),已知SP(f(x),a,g(y),b),求S的原子集, 給出P(f(x),a,g(y),b)的一個基例。已知SP(x) Q(y),R(z) ,求S的原子集, 分別給出P(x) Q(y), R(z)的所有基例。已知S Q(a)P(f(x),Q(b) P(g(x,y), 求S的原子集, 分別給出Q(a)P(f(x) , Q(b) P(g(x,y)的一個基例。設(shè)SP(x), Q(f(y) R(y) ,求S的H域, S的原子集, P(x)的基例, Q(f(y) R(y) 的基例。,.,6/27/2018,6,H解釋,定義(子句集的H解釋) 設(shè)S是子句集,H是S的H域,I*是S在H上的一個解釋稱I*為S的一個H解釋,如果I*滿足如下條件: 1) I*映射S中的所有常量符號到自身。 2)若f是S中n元函數(shù)符號,h1,hn是H中元素,則I*指定映射: (h1,hn) f (h1,hn) 設(shè)A=A1,A2,An, 是S的原子集。于是S的一個H解釋I可方便地表示為如下一個集合: I* m1,m2,mn,其中, mi =,.,6/27/2018,7,H解釋的例子,例 S=P(x)Q(x), R(f(y) S的H域=a, f(a), f(f(a), S的原子集: A=P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), S的H解釋: I1* = P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), I2* = P(a), Q(a), R(a), P(f(a), Q(f(a), R(f(a), ,.,6/27/2018,8,練習(xí),S=P(x)Q(x), P(a), Q(b) ,求S的所有H解釋。,.,6/27/2018,9,二、Herbrand解釋與普通解釋的關(guān)系,子句集S的H解釋是S的普通解釋。S的普通解釋不一定是S的H解釋:普通解釋不是必須定義在H域上,即使定義在H域上,也不一定是一個H解釋。任取普通解釋I,依照I,可以按如下方法構(gòu)造S的一個H解釋I*,使得若 S在 I下為真則 S在I*下也為真。,.,6/27/2018,10,例.,SP(x), Q(y,f(y,a)令S的一個解釋I如下: D1,2 a f(1, 1) f(1, 2) f(2, 1) f(2, 2) 2 1 2 2 1 P(1) P(2) Q(1, 1) Q(1, 2) Q(2, 1) Q(2, 2) T F F T F T對應(yīng)于I的H解釋I*: I*P(a), Q(a, a), P(f(a, a), Q(a, f(a, a), Q(f(a, a), a), Q(f(a, a), f(a, a), ,.,6/27/2018,11,例,S=P(x), Q(y, f(y, z)令S的一個解釋I如下: D=1, 2 f(1, 1) f(1, 2) f(2, 1) f(2, 2) 1 2 2 1 P(1) P(2) Q(1, 1) Q(1, 2) Q(2, 1) Q(2, 2) T F F T F T指定 a對應(yīng)1得H解釋:I1*P(a), Q(a, a), P(f(a, a), Q(a, f(a, a), Q(f(a, a), a), Q(f(a, a), f(a, a), 指定 a對應(yīng)2得H解釋: I2*P(a), Q(a, a), P(f(a, a), Q(a, f(a, a), Q(f(a, a), a), Q(f(a, a), f(a, a), ,.,6/27/2018,12,對應(yīng)于I的H解釋I*,定義(對應(yīng)于I的H解釋I*) 設(shè)I是子句集S在區(qū)域D上的解釋。H是S的H域。 是如下遞歸定義的H到D的映射: 1) 若S中有常量符號,H0是出現(xiàn)在S中所有常量符號的集合。 對任意aH0,規(guī)定 (a)=I(a) 若S中無常量符號,H0=a。 規(guī)定 (a)=d,dD。 2)對任意(h1,hn)Hin,及S中任意n元函數(shù)符號f(x1,xn) , 規(guī)定(f(h1,hn) =I(f(h1,hn) 。,.,6/27/2018,13,對應(yīng)于I的H解釋I*,對應(yīng)于I的H解釋I*是如下的一個H解釋: 任取S中n元謂詞符號P(x1,xn), 任取(h1,hn)Hn,規(guī)定 TI*(P(h1,hn)=TI(P(h1,hn),.,6/27/2018,14,引理 如果某區(qū)域D上的解釋I滿足子句集S, 則對應(yīng)于I的任意一個H解釋I*也滿足S。證明:令S= x1 xn (C1 Cm),其中Ci為子句(i=1, ,m)。由已知TI(S)=T,即對任意(x1,xn)Dn,都有TI(Ci(x1,xn))=T, i=1, ,m,.,6/27/2018,15,因為對S中任意r元謂詞符號P(x1,xr)和任意(h1,hr)Hr,都有TI*( P(h1,hr))=TI(P(h1,hr))其中(h1,hr)Dr。所以,對任意(h1,hn)Hn,都有TI*( Ci(h1,hn))=TI(Ci(h1,hn)) 其中(h1,hn)Dn。 i=1, ,m。 故對任意(h1,hn)Hn ,都有 TI*(Ci(h1,hn))=T, 故TI*(S)=T,即I*滿足S。,.,6/27/2018,16,只考慮子句集的H解釋是否夠用?定理 子句集S恒假當(dāng)且僅當(dāng)S被其所有H解釋弄假。證明: 必要性顯然。充分性。假設(shè)S被其所有H解釋弄假,而S又是可滿足的。設(shè)解釋I滿足S,于是由引理知,對應(yīng)于I的H解釋I*也滿足S,矛盾故S是不可滿足的從現(xiàn)在起,如不特別指出,提到的解釋都是指H解釋,.,6/27/2018,17,結(jié)論,l)子句 C的基例 C被解釋 I滿足,當(dāng)且僅當(dāng) C中的一個基文字L出現(xiàn)在 I中C= P(x) Q(f(y),a) R(z)C= P(a) Q(f(a),a) R(f(a),.,6/27/2018,18,2)子句C被解釋I滿足,當(dāng)且僅當(dāng) C的每一個基例都被I滿足3)子句 C被解釋 I弄假,當(dāng)且僅當(dāng) 至少有一個C的基例C被I弄假。,.,6/27/2018,19,例.,C=P(x)Q(f(x)I1=P(a),Q(a),P(f(a),Q(f(a),P(f(f(a),Q(f(f(a),I2=P(a),Q(a),P(f(a),Q(f(a),P(f(f(a),Q(f(f(a),I3=P(a),Q(a),P(f(a),Q(f(a),P(f(f(a),Q(f(f(a), 顯然,I1,I2滿足C,I3弄假C。,.,6/27/2018,20,4)子句集S不可滿足,當(dāng)且僅當(dāng) 對每個解釋I,至少有一個S中某個子句C的基例C被I弄假。,.,6/27/2018,21,6.2 Herbrand定理,Herbrand定理是符號邏輯中一個很重要的定理Herbrand定理就是使用語義樹的方法,把需要考慮無窮個H解釋的問題,變成只考慮有限個解釋的問題,.,6/27/2018,22,一、語義樹,定義(互補對) 設(shè) A是原子,兩個文字A和A都是另一個的補,集合A,A稱為一個互補對定義(Tautology,重言式) 含有互補對的子句,.,6/27/2018,23,定義 (語義樹) 設(shè)S是子句集,A是S的原子集關(guān)于S的語義樹是一棵向下生長的樹T在樹的每一節(jié)上都以如下方式附著A中有限個原子或原子的否定: 1)對于樹中每一個節(jié)點N,只能向下引出有限的直接的節(jié) L1,Ln 設(shè)Qi是附著在Li上所有文字的合取,i=1, ,n, 則Q1Qn是一個恒真的命題公式2)對樹中每一個節(jié)點 N,設(shè) I(N)是樹T由根向下到節(jié)點 N 的所有節(jié)上附著文字的并集, 則I(N)不含任何互補對,語義樹,.,6/27/2018,24,完全語義樹,定義(完全語義樹) 設(shè)A=A1,An,是子句集S的原子集 S的一個語義樹是完全的,當(dāng)且僅當(dāng) 對于語義樹中每一個尖端節(jié)點N(即從N不再 生出節(jié)的那種節(jié)點),都有 Ai或Ai有且僅有一個屬于I(N),i=1,k,.,6/27/2018,25,例. 設(shè)A=P,Q,R是子句集S的原子集,完全語義樹(正規(guī)完全語義樹 ),.,6/27/2018,26,.,6/27/2018,27,例. 設(shè) S=P(x), Q(f(x)S的原子集為A=P(a), Q(a), P(f(a), Q(f(a), P(f(f(a), Q(f(f(a), ,.,6/27/2018,28,語義樹與解釋,S的完全語義樹的每一個分枝都對應(yīng)著S的一個解釋;定義(部分解釋)對于子句集S的語義樹中的每一個節(jié)點N,I(N)是S的某個解釋的子集,稱I(N)為S的部分解釋。S的任意解釋都對應(yīng)著S的完全語義樹中的一條分枝?綜合: 子句集S的一棵完全語義樹對應(yīng)著S的所有解釋。,.,6/27/2018,29,證明: 若不然,設(shè)T中節(jié)點N向下生出的n個節(jié)L1,Ln的每個節(jié)Li上,都至少有一個文字Ai不在I中由語義樹的定義知:Q1Qn是恒真公式,其中Qi表示Li上所有文字的合取,i=1, , n。將Q1Qn化為合取范式:Q1Qn(A1A2An)() ()因為每一個析取式中都必須有一個互補對。不妨設(shè)A1A2,于是A2,A2都不在I中,這與I是一個解釋矛盾。結(jié)論:對S的任意解釋I,都可以從S的完全語義樹的根點出發(fā),向下找出一條分枝,使該分枝對應(yīng)著解釋I。,引理 設(shè)T是子句集S的完全語義樹,I是S的一個解釋。于是T中任意節(jié)點向下生出的直接節(jié)中,必有一節(jié),其上所有文字都在I中。,.,6/27/2018,30,子句集的封閉語義樹,定義(失效點) 稱語義樹T中的節(jié)點N為失效點,如果(1)I(N)弄假S中某個子句的某個基例;(2)I(N)不弄假S中任意子句的任意基例,其中N是 N的任意祖先節(jié)點。定義(封閉語義樹) 語義樹T是封閉的,當(dāng)且僅當(dāng)T的每個分枝的終點都是失效點。定義(推理點)稱封閉語義樹的節(jié)點 N為推理點,如果N的所有直接下降節(jié)點都是失效點,.,6/27/2018,31,例. 設(shè)S=P, PR, PQ, PR。,S的原子集 A=P, Q, R,P,P,Q,Q,Q,Q,R,R,R,R,R,R,R,R,.,6/27/2018,32,練習(xí),設(shè)子句集S=P(x)Q(x),P(f(x), Q(f(x)分別畫出S的完全語義樹與 封閉語義樹。,.,6/27/2018,33,二、Herbrand定理,Herbrand定理I子句集S是不可滿足的,當(dāng)且僅當(dāng)對應(yīng)于S的每一個完全語義樹都存在一個有限的封閉語義樹證明: 必要性:若S是不可滿足的,設(shè)T是S的完全語義樹 對T的每一個分枝B,令I(lǐng)B是附著在B上所有文字的集合,則IB是S的一個解釋,故IB弄假S中某子句C的某個基例C由于C是有限的,所以B上存在一個節(jié)點NB使得部分解釋I(NB)弄假C,于是分枝B上存在失效點因此,對T中每一分枝都存在一個失效點,于是從T得到S的一個封閉語義樹T。,.,6/27/2018,34,Herbrand定理I子句集S是不可滿足的,當(dāng)且僅當(dāng)對應(yīng)于S的每一個完全語義樹都存在一個有限的封閉語義樹,(有限性) 因為封閉語義樹T中每一個節(jié)點只能向下生長有限個節(jié),故T必有有限個節(jié)點.否則,由Konig無限性引理,T中必有一條無窮的分枝,此無窮分枝上當(dāng)然沒有失效點,矛盾。(Konig無限性引理:在一個其點之次數(shù)有限的無限有向樹中,必有一源于根的無限路。 )充分性:若S的每一個完全語義樹T都對應(yīng)著一個有限封閉語義樹T,則T的每條分枝上都有一個失效點。因為S的任一解釋都對應(yīng)T的某一條分枝,所以每一個解釋都弄假S, 故S是不可滿足的。,.,6/27/2018,35,Herbrand定理II 子句集S是不可滿足的,當(dāng)且僅當(dāng)存在S的一個有限不可滿足的S的基例集S。,證明: 必要性:若S恒假,設(shè)T是S的完全語義樹,由Herbrand定理I知,有一個有限封閉語義樹 T對應(yīng)著T。令S是被 T中所有失效點弄假的所有基例(S中某些子句的基例)的集合。因為T中失效點的個數(shù)有限,所以S是有限集合。任取S的一解釋I,則I是S的某個解釋I的子集,而解釋I是T中一個分枝,所以,I弄假S中子句C,故I弄假S。因為II,且I是S的解釋,故I弄假S由I的任意性知S不可滿足。,S=P(x), P(a)P(b), Q(f(x)H=a,b,f(a),f(b),f(f(a),f(f(b),A=P(a),P(b),Q(a),Q(b),S=P(a), P(b), P(a)P(b),.,6/27/2018,36,Herbrand定理II 子句集S是不可滿足的,當(dāng)且僅當(dāng)存在S的一個有限不可滿足的S的基例集S。,充分性:假設(shè)S有一個有限的不可滿足的基例集S。 任取S的解釋I, 因為S的每一個解釋I都包含著S的一個解釋I,而S是不可滿足的,所以S的任一解釋I都弄假S,故I弄假S中至少一個子句,即I弄假S中至少一個子句的基例,亦即I弄假S。 由I的任意性,知S是不可滿足的。,.,6/27/2018,37,Herbrand定理II提出了一種證明子句集S的不可滿足性的方法:如果存在這樣一個機械程序,它可以逐次生成S中子句的基例集 S0,Sn,并逐次地檢查S0,Sn,的不可滿足性,那么根據(jù) Herbrand定理,如果 S是不可滿足的,則這個程序一定可以找到一個有限數(shù)N,使SN是不可滿足的。,.,6/27/2018,38,使用Herbrand定理的機器證明過程,Gilmore過程D-P過程,.,6/27/2018,39,Gilmore過程(1960年),逐次地生成S0, S1,Sn,其中Si是用S的i級常量集合Hi中的常量,代替S中子句的變量,而得到的S的所有基例之集合。對于每一個Si,可以使用命題邏輯中的任意的方法去檢查Si的不可滿足性。 Gilmore使用了所謂乘法方法:即將Si化為析取范式。如果其中任意一個合取項包含一個互補對,則可以刪除這個合取項,最后,如果某個Si是空的,則Si是不可滿足的。當(dāng)S不可滿足時,該算法一定結(jié)束(半可判定)。,.,6/27/2018,40,例. S=P(a), P(x) Q(f(x), Q(f(a) H0=a S0=P(a) (P(a) Q(f(a) Q(f(a) =(P(a)P(a)Q(f(a)(P(a) Q(f(a)Q(f(a) = =所以,S是不可滿足的。該算法具有指數(shù)復(fù)雜性,為此提出了改進(jìn)規(guī)則,稱為Davis-Putnam預(yù)處理-檢驗基子句集不可滿足性。,.,6/27/2018,41,D-P過程,設(shè)S是基子句集Tautology刪除規(guī)則 設(shè)S為刪去S中所有的Tautology所剩子句集, 則 S恒假 iff S恒假。,.,6/27/2018,42,單文字規(guī)則 若S中有一個單元基子句L,令S為刪除S中包含L的所有基子句所剩子句集,則:(1) 若S為空集,則S可滿足。(2) 否則, 令S為刪除S中所有文字L所得子句集 (若S 中有單元基子句L,則刪文字L 得空子句), 于是, S恒假 iff S恒假。S=L(LC1) (LCi) (LCi+1) (LCj) Cj+1 Cn,.,6/27/2018,43,定義(純文字):稱S的基子句中文字L是純的,如果L不出現(xiàn)在S中。純文字規(guī)則設(shè)L是S中純文字,且S為刪除S中所有包含L的基子句所剩子句集,則(1)若S為空集,則S可滿足。(2) 否則,S恒假 iff S恒假。S=(LC1) (LCi) Ci+1 Cn,.,6/27/2018,44,分裂規(guī)則若S=(A1 L) (Am L) (B1 L) (Bn L) R 其中A i , Bi ,R都不含L或L,令 S1 =A1 Am RS2= B1 Bn R 則S恒假 iff S1 , S2同時恒假。,.,6/27/2018,45,Davis-Putnam方法練習(xí),S= (PQR) (PQ) P R US= (PQ) (PQ) (QR) (QR) S= (PQ) (PQ) (RQ) (RQ),.,6/27/2018,46,Herbrand定理的主要障礙,要求生成關(guān)于子句集S的基例集 S1, S2, 。在多數(shù)情況下,這些集合的元數(shù)是以指數(shù)方式增加的:例.S=P(x,g(x),y,h(x,y),z,k(x,y,z),P(u,v,e(v),w,f(v,w),x) H0=a H1=a, g(a), h(a, a), k(a, a, a), e(a), f(a, a) S0=P(a,g(a),a,h(a,a),a,k(a,a,a),P(a,a,e(a),a,f(a,a),a) S1=(666)+(6666)=216+1296=1512個元素 S5是不可滿足的,但是H5是1065數(shù)量級個元素,而S5有10260數(shù)量級的元素。想將S5存儲起來都是不可能的,更不要說是檢查它的不可滿足性了。,.,6/27/2018,47,為了避免像Herbrand定理所要求的那樣去生成子句的基例集,J.A.Robinson于1965年提出了歸結(jié)原理,歸結(jié)原理可以直接應(yīng)用到任意子句集S上(不一定是基子句集),去檢查S的不可滿足性。歸結(jié)原理的本質(zhì)思想是去檢查子句集S是否包含一個空子句: 如果S包含,則S是不可滿足的。 如果S不包含,則去檢查是否可由S推導(dǎo)出來。 當(dāng)然這個推理規(guī)則必須保證推出的子句是原親本子句的邏輯結(jié)果。歸結(jié)原理就是具有這種性質(zhì)的一種推理規(guī)則。,歸結(jié)原理思想,.,6/27/2018,48,命題邏輯中的歸結(jié)原理,.,6/27/2018,49,歸結(jié)式,定義(歸結(jié)式) 對任意兩個基子句C1和C2。如果C1中存在文字L1,C2中存在文字L2,且L1L2, 則從C1和C2中分別刪除L1和L2,將C1和C2的剩余部分析取起來構(gòu)成的子句,稱為C1和C2的歸結(jié)式,記為R(C1, C2)。 C1和C2稱為親本子句。,.,6/27/2018,50,練習(xí):求下述各子句對的歸結(jié)式,C1= PQR, C2=QSC1= PQR, C2=P RQ,.,6/27/2018,51,定理 設(shè)C1和C2是兩個基子句, R(C1, C2) 是C1,C2的歸結(jié)式,則R(C1, C2)是C1和C2的邏輯結(jié)果。證明: 設(shè) C1=L C1, C2=LC2。于是 R(C1, C2) C1 C2 設(shè)I是C1和C2的一個解釋,且滿足C1也滿足C2。因為L和L中有一個在I下為假,不妨設(shè)為L。于是C1非空,且在I下為真。故R(C1, C2)在I下為真。,命題邏輯歸結(jié)方法的可靠性,.,6/27/2018,52,歸結(jié)演繹,定義(歸結(jié)演繹) 設(shè)S是子句集。從S推出子句C的一個歸結(jié)演繹是如下一個有限子句序列: C1,C2,Ck其中Ci或者是S中子句,或者是Cj和Cr的歸結(jié)式 (ji, r i);并且CkC。 稱從子句集S演繹出子句C,是指存在一個從S推出C的演繹。定理 若從子句集S可以演繹出子句C,則C是S的邏輯結(jié)果。推論 若子句集S是可滿足的, 則S推出的任意子句也是可滿足的。,.,6/27/2018,53,定義 從S推出空子句的演繹稱為一個反駁(反證) ,或稱為S的一個證明。結(jié)論:若從基子句集S可演繹出空子句,則S是不可滿足的。演繹樹:從子句集S出發(fā),通過歸結(jié)原理可得到一個向下的演繹樹,其每個初始節(jié)點上附著一個S中子句,每個非初始節(jié)點上附著一個其前任節(jié)點上子句的歸結(jié)式。,.,6/27/2018,54,例. S=PQ, PQ, PQ, PQ ,歸結(jié)演繹: (1) PQ (2) PQ (3) PQ (4) PQ (5) Q 由(1)、(2) (6) Q 由(3)、(4) (7) 由(5)、(6),.,6/27/2018,55,歸結(jié)原理一般過程:,1)建立子句集S。2)如果S含空子句,則結(jié)束。3)從子句集S出發(fā),僅對S的子句間使用歸結(jié)推理規(guī)則。4)如果得出空子句,則結(jié)束。5)將所得歸結(jié)式仍放入S中。6)對新的子句集使用歸結(jié)推理規(guī)則。轉(zhuǎn)4)。,.,6/27/2018,56,例.證明(P Q) Q p,首先建立子句集:S=PQ, Q , P歸結(jié)演繹:(1) P Q(2) Q(3) P(4) P (1)(2)歸結(jié)(5) (3)(4)歸結(jié),.,6/27/2018,57,命題邏輯歸結(jié)原理的完備性,定理 如果基子句集S是不可滿足的, 則存在從S推出空子句的歸結(jié)演繹。證明: 設(shè)M是S的原子集,對M的元素數(shù)|M|用歸納法。 當(dāng)|M|=1時,設(shè)原子為P。 若S ,得證。 否則,因為S是不可滿足的,于是,S中必包含單元子句P和P,而P和P的歸結(jié)式是,所以存在從S推出的歸結(jié)演繹。 假設(shè)|M|n (n2) 時,定理成立。往證 |M|n時定理成立。,.,6/27/2018,58,取M中任意一原子P,做如下兩個子句集:S:將S中所有含P的子句刪除,然后在剩下的子 句中刪除文字P;S”:將S中所有含P的子句刪除,然后在剩下的 子句中刪除文字P。顯然,S和S”都不可滿足,且它們的原子集的元素數(shù)都小于n。根據(jù)歸納假設(shè),存在從S推出 的歸結(jié)演繹D1,從S”推出的歸結(jié)演繹D2。,.,6/27/2018,59,S=PC1, ,PCi , PCi+1, ,PCj, Cj+1 , , CnS=Ci+1, ,Cj,Cj+1 , , CnS=C1, ,Ci , Cj+1 , , Cn例:S=PQ, PQ, PR, RM=P,Q,R,.,6/27/2018,60,在D1中,將S中所有不是S中的子句,通過添加文字P而恢復(fù)成S中子句,于是,得到從S推出 或者P的歸結(jié)演繹D1。 用同樣方法從D2可得一個從S推出 或者P的歸結(jié)演繹D2。 顯然,從D1和D2就不難得到一個從S推出 的歸結(jié)演繹D。歸納法完成。,.,6/27/2018,61,Resolution Principle 兩種譯法:歸結(jié)原理:從內(nèi)部看 劉敘華,一種新的語義歸結(jié)原理,吉林大學(xué)學(xué)報,1978。消解原理:從外部看 馬希文,機器證明及其應(yīng)用,計算機應(yīng)用, 1978。,.,6/27/2018,62,6.3 合一算法,.,6/27/2018,63,例1 C1:P(x) Q(y) C2:P(a) R(z)例2 C1:P(x) Q(x) C2:P(f(x) R(x)替換和合一是為了處理謂詞邏輯中子句之間的模式匹配而引進(jìn).,.,6/27/2018,64,一、替換與最一般合一替換,定義(替換)一個替換是形如t1/v1, , tn/vn 的一個有限集合,其中vi是變量符號,ti是不同于vi的項。并且在此集合中沒有在斜線符號后面有相同變量符號的兩個元素,稱ti為替換的分子,vi為替換的分母。例. a/x, g(y)/y, f(g(b)/z是替換; x/x, y/f(x), a/x, g(y)/y, f(g(b)/y不是替換;基替換:當(dāng)t1,tn是基項時,稱此替換為基替換。空替換:沒有元素的替換稱為空替換,記為。,.,6/27/2018,65,替換,定義(改名) 設(shè)替換 = t1/x1, , tn/xn 如果t1, , tn是不同的變量符號,則稱為一個改名替換,簡稱改名。替換作用對象:表達(dá)式(項、項集、原子、原子集、 文字、子句、子句集)基表達(dá)式:沒有變量符號的表達(dá)式。子表達(dá)式:出現(xiàn)在表達(dá)式E中的表達(dá)式稱為E的子 表達(dá)式。,.,6/27/2018,66,E的例,定義(E的例) 設(shè) = t1/v1, , tn/vn 是一個替換,E是一個表達(dá)式。將E中出現(xiàn)的每一個變量符號,vi (1 i n) ,都用項ti替換,這樣得到的表達(dá)式記為E。稱E 為E的例。 若E 不含變量,則E 為E的基例。例. 令 = a/x, f(b)/y, c/z,E=P(x, y, z)于是E的例(也是E的基例)為 E = P(a, f(b), c),.,6/27/2018,67,練習(xí): E=P(x, g(y), h(x,z), =a/x, f(b)/y, g(w)/zE=P(a, g(f(b), h(a,g(w) E=P(x, y, z), =y/x, z/y E=P(y, z, z). EP(z, z, z).,.,6/27/2018,68,替換的乘積,定義(替換的乘積)設(shè) = t1/x1, , tn/xn , = u1/y1, , um/ym 是兩個替換。將下面集合 t1/x1, , tn/xn , u1/y1, , um/ym 中任意符合下面條件的元素刪除: 1)ui/yi,當(dāng)yix1, , xn 時; 2)ti/xi,當(dāng)ti = xi 時。如此得到一個替換,稱為與的乘積,記為 。例. 令 =f(y)/x, z/y =a/x, b/y, y/z 于是得集合 t1/x1, t2/x2 , u1/y1, u2/y2 , u3/y3 = f(b)/x, y/y, a/x, b/y, y/z 與的乘積為 = f(b)/x, y/z ,.,6/27/2018,69,=a/x, =b/x =a/x =b/x可見: ,.,6/27/2018,70,例子:E=P(x, y, z)=a/x, f(z)/y, w/zE=P(a, f(z), w)=t/z, g(b)/w(E)=P(a, f(t), g(b)=a/x, f(t)/y, g(b)/z,g(b)/wE=P(a, f(t), g(b),.,6/27/2018,71,引理 若E是表達(dá)式,是兩個替換, 則E ( ) = (E),證明: 設(shè)vi是E中任意一個變量符號,而 = t1/x1, , tn/xn , = u1/y1, , um/ym 若vi既不在 x1, , xn 中,也不在 y1, , ym 中,則vi在E ( )中和在(E)中都不變。若vi=xj (1jn),則E中的vi,在(E)中先變成tj,然后再變成tj;E中的vi在E()中立即就變成了tj。故E中vi在(E)中和在E()中有相同變化。若vi=yj (1jm),且yj x1,xn ,則E中vi在(E)中變?yōu)閡j;E中vi在E()中也變?yōu)閡j(注意:yjx1, xn,所以uj/yj),故E中vi在(E)中和在E ()中有相同變化。 由于vi的任意性,故引理得證。,.,6/27/2018,72,引理 設(shè), 是三個替換, 于是()(),證明: 設(shè)E是任一表達(dá)式,由上面引理知 E() =(E() = (E) E() =(E) () = (E) 所以 E() = E()由于E的任意性,故 ()(),.,6/27/2018,73,定義(合一)稱替換是表達(dá)式集合E1,Ek的 合一,當(dāng)且僅當(dāng)E1E2=Ek。 表達(dá)式集合E1, , Ek稱為可合一的,如果存在關(guān)于此集合的一個合一。定義(最一般合一) 表達(dá)式集合E1, , Ek的合一 稱為是最一般合一(most general unifier, 簡寫為mgu),當(dāng)且僅當(dāng)對此集合的每一個合一,都存在替換,使得,.,6/27/2018,74,例. 表達(dá)式集合P(a, y), P(x, f(b)是可合一的,其最一般合一a/x, f(b)/y。顯然,這也是此集合的mgu。? 表達(dá)式集合P(a, b), P(x, f(b)是否可合一?例. 表達(dá)式集合P(x), P(f(y)是可合一的,其最一般合一f(y)/x f(a)/x, a/y也是合一,有替換 =a/y,使=f(y)/xa/y,.,6/27/2018,75,例 S=P(x) Q(x),P(y), Q(b) P(x),P(y)可合一,a/x, a/y是合一, 其mgu x/y,有替換 =a/x,使= x/y a/x,.,6/27/2018,76,二、合一算法,定義(差異集合) 設(shè)W是非空表達(dá)式集合,W的差異集合是如下一個集合:首先找出W的所有表達(dá)式中不是都相同的第一個符號,然后從W的每一個表達(dá)式中抽出占有這個符號位置的子表達(dá)式。所有這些子表達(dá)式組成的集合稱為這步找到的W的差異集合D。,.,6/27/2018,77,W不可合一的三種情況,(1)若D中無變量符號為元素,則W是不可合一的。例. W=P(f(x), P(g(x) D=f(x), g(x) (2)若D中有奇異元素和非奇異元素,則W是不可合一的。例. W=P(x), P(x, y) D=, y(3)若D中元素有變量符號x和項t,且x出現(xiàn)在t中,則W是不可合一的。例. W=P(x), P(f(x) D=x, f(x),.,6/27/2018,78,換名:P(f(x), x), P(x, a);如果不換名:D=f(x), x.換名: P(f(y), y), P(x, a);mgu: f(a)/x, a/y,.,6/27/2018,79,步驟1:置 k=0, Wk=W, k=步驟2:若Wk只有一個元素,則停止,k是W的最一般合一; 否則,找出Wk的差異集合Dk。步驟3:若Dk非奇異,Dk中存在元素vk和tk,其中vk是變量符號,并且 不出現(xiàn)在tk中,則轉(zhuǎn)步驟4; 否則,算法停止,W是不可合一的。步驟4:令 k+1=ktk/vk,Wk+1=Wk (注:Wk+1=W )步驟5:置 k=k+1,轉(zhuǎn)步驟2。,合一算法(Unification algorithm),.,6/27/2018,80,例. 令 W=Q(f(a), g(x), Q(y, y), 求W的mgu。,步驟1: k=0, W0=W, 0=。步驟2: D0 =f(a), y。步驟3:有v0= y D0,v0不出現(xiàn)在t0f(a)中。步驟4:令 1=0t0/v0=f(a)/y, W1=Q(f(a), g(x), Q(f(a), f(a)步驟5:k=k+1=1步驟2: D1 =g(x), f(a) 。步驟3:D1中無變量符號,算法停止,W不可合一。? 若令W=Q(f(a), g(x), Q(y, z), W是否可合一?,.,6/27/2018,81,例 令 W= P(a, x, f(g(y), P(z, f(z), f(u), 求出W的mgu。,步驟1:k=0,W0=W, 0= 。步驟2: D0 =a, z。步驟3:有v0= z D0,v0不出現(xiàn)在t0a中。步驟4:令 1=0t0/v0=a/z=a/z,W1=W0t0/v0=P(a,x,f(g(y),P(z,f(z),f(u)a/z=P(a,x,f(g(y),P(a,f(a),f(u)步驟5:k=k+1=1步驟2: D1 =x, f(a) 。步驟3:有v1= x D1,且v1不出現(xiàn)在t1f(a)中。步驟4:令 2=1t1/v1=a/z f(a)/x =a/z, f(a)/x ,W2=W1t1/v1=P(a,x,f(g(y),P(a,f(a),f(u)f(a)/x =P(a,f(a),f(g(y),P(a,f(a),f(u),.,6/27/2018,82,例.,步驟5:k=k+1=2步驟2: D2 =g(y), u。步驟3:有v2= u D2,且v2不出現(xiàn)在t2g(y)中。步驟4:令 3=2t2/v2=a/z, f(a)/x g(y)/u =a/z, f(a)/x, g(y)/u ,W3=W2t2/v2=P(a, f(a), f(g(y), P(a, f(a), f(u) g(y)/u =P(a, f(a), f(g(y)步驟5:k=k+1=3步驟2:W3只有一個元素。算法停止。 3=a/z, f(a)/x, g(y)/u 是W的最一般合一。,.,6/27/2018,83,定理 若W是關(guān)于表達(dá)式的有限非空可合一集合,則合一算法終將結(jié)束在步驟2,并且最后的k是W的最一般合一。,證明: (1)終止性。否則將產(chǎn)生一個無窮序列:W , W , W ,其中每一個直接后繼集合比它的前任都少一個變量符號(注意:W 包含vk,而W 不包含vk)。但這是不可能的,因為W僅含有限個變量符號。 (2) k是W的合一。若算法停止在步驟2,則Wk=W只含有一個元素,所以k是W的合一。,.,6/27/2018,84,(3)用歸納法證明算法必不會停止在步驟3,并且對任意W的一個合一,任意k,都存在替換k,使得 =kk 亦即k是W的mgu。 當(dāng)k=0時,因0=,取0=,于是=00。,.,6/27/2018,85,假設(shè)對0kn,=kk成立。 往證:存在n+1,使得=n+1n+1。若W 只含有一個元素,則合一算法結(jié)束在步驟2。因為=nn,且n是W的合一,故n是W的mgu。定理得證。 若W 不只含有一個元素,按照算法,將找出W的差異集合Dn。因為=nn是W的合一,所以W中表達(dá)式經(jīng)替換作用后都變成同一個相同的表達(dá)式。而W中表達(dá)式經(jīng)n作用后,產(chǎn)生了差異集合Dn,所以Dn必須被n所統(tǒng)一,即n是D n的合一。,.,6/27/2018,86,因為Dn是可合一的(n就是Dn的合一),所以必有變量符號vnDn;Dn中至少有兩個不同元素。所以可設(shè)tnDn,且tnvn。顯然,變量符號vn不出現(xiàn)在tn中(否則,vnn tnn,這與n是Dn的合一矛盾)。 因此算法不能停止在步驟3,所以算法必然停止在步驟2。,.,6/27/2018,87,令n+1=ntn/vn。因為vnn=tnn,所以tnn/vnn令n+1=n -tnn/vn。因vn不出現(xiàn)在tn中,所以于是 故歸納法完成。即對所有k0,都存在替換k,使=kk。所以算法終止步驟2時,k是W的最一般合一。,.,6/27/2018,88,6.4 一階邏輯中的歸結(jié)原理,.,6/27/2018,89,定義(因子) 如果子句C中,兩個或兩個以上的文字有一個最一般合一,則C稱為C的因子; 如果C是單元子句,則C稱為C的單因子。例. C=P(x) P(f(y) Q(x) 令 f(y)/x,于是 C= P(f(y) Q(f(y) 是C的因子。,.,6/27/2018,90,二元歸結(jié)式,定義 設(shè)C1, C2是兩個無公共變量的子句(稱為親本子句), L1, L2分別是C1, C2中的兩個文字。 如果L1和L2有最一般合一 ,則子句 (C1- L1) ( C2- L2) 稱為C1和C2的二元歸結(jié)式,L1和L2稱為歸結(jié)文字。例. 設(shè)C1=P(x) Q(x), C2=P(a) R(x)將C2中x改名為y。取L1P(x), L2=P(a), =a/x, 于是(C1- L1) ( C2- L2)(P(a), Q(a)-P(a) (P(a), R(y)-P(a)=Q(a), R(y)= Q(a) R(y) -C1和C2的二元歸結(jié)式.,.,6/27/2018,91,練習(xí):設(shè)C1=P(a) R(x), C2=P(y) Q(b) 求C1和C2的二元歸結(jié)式.,.,6/27/2018,92,在謂詞邏輯中,對子句進(jìn)行歸結(jié)推理時,要注意的幾個問題:(1)若被歸結(jié)的子句C1 和C2中具有相同的變元時,需要將其中一個子句的變元更名,否則可能無法合一,從而沒有辦法進(jìn)行歸結(jié)。,.,6/27/2018,93,例: C1=P(x), C2=P(f(x) 例:設(shè)知識庫中有如下知識:(1)若x的父親是y,則x不是女人。(2)若x的母親是y,則x是女人。(3)Chris的母親是Mary。(4)Chris的父親是Bill。求證:這些斷言包含有矛盾。 father(x,y):x的父親是y mother(x,y):x的母親是y woman(x):x是女人,.,6/27/2018,94,(2)在求歸結(jié)式時,不能同時消去兩個互補文字對,消去兩個互補文字對所得的結(jié)果不是兩個親本子句的邏輯推論。例.設(shè)C1=P(x) Q(b), C2=P(a) Q(y)R(z) 求C1和C2的二元歸結(jié)式.(3)如果在參加歸結(jié)的子句內(nèi)含有可合一的文字,則在進(jìn)行歸結(jié)之前,應(yīng)對這些文字進(jìn)行合一,以實現(xiàn)這些子句內(nèi)部的化簡。,.,6/27/2018,95,歸結(jié)式,定義 子句C1, C2的一個歸結(jié)式是下列二元歸結(jié)式之一:C1和C2的二元歸結(jié)式。C1和C2的因子的二元歸結(jié)式。C1的因子和C2的二元歸結(jié)式。C1的因子和C2的因子的二元歸結(jié)式。例. 設(shè) C1=P(x) P(f(y) R(g(y) C2=P(f(g(a) Q(b)C1的因子C1= P(f(y) R(g(y)。于是C1和C2的二元歸結(jié)式,從而也是C1和C2的歸結(jié)式為 R(g(g(a) Q(b),.,6/27/2018,96,一階邏輯歸結(jié)原理的完備性,提升引理 如果C1和C2分別是子句C1和C2的例,C是C1和C2的歸結(jié)式,則存在C1和C2的一個歸結(jié)式C,使C是C的例。例 C1:P(x) Q(f(x) C2: Q(y) R(y) C1: P(a) Q(f(a) C2:Q(f(a) R(f(a) C : P(a) R(f(a) C: P(x) R(f(x),.,6/27/2018,97,一階邏輯歸結(jié)原理的完備性,定理 若子句集S是不可滿足的,則存在從S推出空子句的歸結(jié)演繹。 證明: 設(shè)子句集S是不可滿足的,由Herbrand定理II知,存在S的一個基例集S也是不可滿足的。 根據(jù)命題邏輯歸結(jié)原理的完備性,存在從S推出空子句的歸結(jié)演繹D。 由提升引理知,可將D提升成一個從S推出空子句的歸結(jié)演繹D。定理得證。,.,6/27/2018,98,應(yīng)用歸結(jié)原理的習(xí)題,.,6/27/2018,99,6.5 歸結(jié)原理的幾種改進(jìn),.,6/27/2018,100,水平浸透法(Level Saturation Method)S0= SSn= C1和C2的歸結(jié)式| C1S0Sn-1,C2 Sn-1,.,6/27/2018,101,例.使用水平浸透法證明 S=PQ,PQ, PQ, PQ 不可滿足。,