魯濱遜歸結(jié)原理

1、第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.2.2 命題邏輯中的歸結(jié)原理命題邏輯中的歸結(jié)原理 歸結(jié)演繹推理是基于一種稱為歸結(jié)原理(亦稱消解原理principleofresolution)的推理規(guī)則的推理方法。歸結(jié)原理是由魯濱遜(J.A.Robinson)于1965年首先提出。它是謂詞邏輯中一個相當(dāng)有效的機(jī)械化推理方法。歸結(jié)原理的出現(xiàn)，被認(rèn)為是自動推理，特別是定理機(jī)器證明領(lǐng)域的重大突破。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義4 設(shè)L為一個文字，則稱乛L與L為互補(bǔ)文字。 定義定義5 設(shè)C1,C2是命題邏輯中的兩個子句，C1中有文字L1，C2中有

2、文字L2，且L1與L2互補(bǔ)，從C1,C2中分別刪除L1,L2，再將剩余部分析取起來，記構(gòu)成的新子句為C12，則稱C12為C1,C2的歸結(jié)式(或消解式)，C1,C2稱為其歸結(jié)式的親本子句， L1,L2稱為消解基。 例例3.9 設(shè)C1=乛PQR,C2=乛QS,于是C1,C2的歸結(jié)式為乛PRS 定理定理2 歸結(jié)式是其親本子句的邏輯結(jié)果。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 證明 設(shè)C1=LC1,C2=乛LC2,C1,C2都是文字的析取式，則C1,C2的歸結(jié)式為C1C2，因為 C1=C1L=乛C1L, C2=乛LC2=(LC2)所以 C1C2=(乛C1L)(LC2) (乛C1C

3、2)=C1C2 證畢。 由定理2即得推理規(guī)則： C1C2 (C1-L1)(C2-L2) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.10 用歸結(jié)原理驗證分離規(guī)則：A(AB) B和拒取式(AB)乛B 乛A。 解 A(AB) A(乛AB) B (AB)乛B (乛AB)(乛B) 乛A 類似地可以驗證其他推理規(guī)則也都可以經(jīng)消解原理推出。這就是說，用消解原理就可以代替其他所有的推理規(guī)則。再加上這個方法的推理步驟比較機(jī)械，這就為機(jī)器推理提供了方便。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 推論 設(shè)C1,C2是子句集S的兩個子句，C12是它們的歸結(jié)式，則 (1)

4、若用C12代替C1,C2，得到新子句集S1，則由S1的不可滿足可推出原子句集S的不可滿足。即 S1不可滿足 S不可滿足 (2)若把C12加入到S中，得到新子句集S2，則S2與原S的同不可滿足。即 S2不可滿足 S不可滿足第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.11 證明子句集PQ,P,Q是不可滿足的。證證(1)P乛Q(2)乛P(3)Q(4)乛Q 由(1),(2)(5) 由(3),(4)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.12 用歸結(jié)原理證明R是P,(PQ)R,(SU)Q,U的邏輯結(jié)果。 證 我們先把諸前提條件化為子句形式，再把結(jié)論

5、的非也化為子句，由所有子句得到子句集S=P,乛P乛QR,乛SQ,乛UQ,U,乛R，然后對該子句集施行歸結(jié)，歸結(jié)過程用下面的歸結(jié)演繹樹表示（見圖31）。由于最后推出了空子句，所以子句集S不可滿足，即命題公式 P(乛P乛QR)(乛SQ)(乛UQ)U乛R 不可滿足，從而R是題設(shè)前提的邏輯結(jié)果。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 圖51 例5.12歸結(jié)演繹樹 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 ABC三人應(yīng)試,經(jīng)面試后公司表示如下想法: (1)三人中至少錄取一人 (2)如果錄取A而不錄取B,則一定錄取C (3)如果錄取B,則一定錄取C 求證:公司一

6、定錄取C作業(yè)： 自然數(shù)都是大于零的整數(shù)，所有整數(shù)不是偶數(shù)就是奇數(shù)，偶數(shù)除以2是整數(shù)。證: 所有自然數(shù)不是奇數(shù)就是其一半為整數(shù)的數(shù)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.2.3 替換與合一替換與合一 在一階謂詞邏輯中應(yīng)用消解原理，不像命題邏輯中那樣簡單，因為謂詞邏輯中的子句含有個體變元，這就使尋找含互否文字的子句對的操作變得復(fù)雜。例如： C1=P(x)Q(x) C2=乛P(a)R(y) 直接比較，似乎兩者中不含互否文字，但如果我們用a替換C1中的x，則得到 C1=P(a)Q(a) C2=乛P(a)R(y)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 于是

7、根據(jù)命題邏輯中的消解原理，得C1和C2的消解式 C3=Q(a)R(y) 所以，要在謂詞邏輯中應(yīng)用消解原理，則一般需要對個體變元作適當(dāng)?shù)奶鎿Q。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義6 一個替換(Substitution)是形如t1/x1,t2/x2,tn/xn的有限集合，其中t1,t2,tn是項，稱為替換的分子；x1,x2,xn是互不相同的個體變元，稱為替換的分母；ti不同于xi，xi也不循環(huán)地出現(xiàn)在tj(i,j=1,2,n)中；ti/xi表示用ti替換xi。若t1,t2,tn都是不含變元的項（稱為基項）時，該替換稱為基替換；沒有元素的替換稱為空替換，記作，它表示

8、不作替換。例如：第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 a/x,g(y)/y , f(g(b)/z就是一個替換，而g(y)/x, f(x)/y則不是一個替換,因為x與y出現(xiàn)了循環(huán)替換。下面我們將項、原子公式、文字、子句等統(tǒng)稱為表達(dá)式，沒有變元的表達(dá)式稱為基表達(dá)式，出現(xiàn)在表達(dá)式E中的表達(dá)式稱為E的子表達(dá)式。 定義定義7 設(shè)=t1/x1,tn/xn是一個替換，E是一個表達(dá)式，把對E施行替換，即把E中出現(xiàn)的個體變元xj(1jn)都用tj替換，記為E，所得的結(jié)果稱為E在下的例(instance)。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義8 設(shè)=t1

9、/x1,tn/xn,=u1/y1,um/ym是兩個替換，則將集合 t1/x1,tn/xn,u1/y1,um/ym 中凡符合下列條件的元素刪除： (1)ti/xi 當(dāng)ti=xi (2)ui/yi當(dāng)yix1,xn 如此得到的集合仍然是一個替換，該替換稱為與的復(fù)合或乘積，記為。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.13 設(shè)=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可以證明，替換的乘積滿足結(jié)合律，即 ()u=(u)第第5 5

10、章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義9 設(shè)S=F1,F2,Fn是一個原子謂詞公式集，若存在一個替換，可使F1=F2=Fn，則稱為S的一個合一(Unifier)，稱S為可合一的。 一個公式集的合一一般不唯一。 定義10 設(shè)是原子公式集S的一個合一，如果對S的任何一個合一，都存在一個替換，使得 = 則稱為S的最一般合一(MostGeneralUnifier)，簡稱MGU。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.14 設(shè)S=P(u,y,g(y),P(x,f(u),z)，S有一個最一般合一 =u/x,f(u)/y,g(f(u)/z 對S的任一合一

11、，例如： =a/x,f(a)/y,g(f(a)/z,a/u 存在一個替換 =a/u 使得 =第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 可以看出，如果能找到一個公式集的合一，特別是最一般合一，則可使互否的文字的形式結(jié)構(gòu)完全一致起來，進(jìn)而達(dá)到消解的目的。如何求一個公式集的最一般合一？有一個算法，可以求任何可合一公式集的最一般合一。為了介紹這個算法，我們先引入差異集的概念。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定義定義11 設(shè)S是一個非空的具有相同謂詞名的原子公式集，從S中各公式的左邊第一個項開始，同時向右比較，直到發(fā)現(xiàn)第一個不都相同的項為止，用這些項的

12、差異部分組成一個集合，這個集合就是原公式集S的一個差異集。 例例3.15 設(shè)S=P(x,y,z),P(x,f(a),h(b)，則不難看出，S有兩個差異集 D1=y,f(a) D2=z,h(b) 設(shè)S為一非空有限具有相同謂詞名的原子謂詞公式集，下面給出求其最一般合一的算法。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 合一算法合一算法(Unification algorithm)：步步1 置k=0, Sk=S，k=;步步2 若Sk只含有一個謂詞公式，則算法停止，k就是要 求的最一般合一;步步3 求Sk的差異集Dk;步步4 若Dk中存在元素xk和tk，其中xk是變元，tk是項且xk

13、 不在tk中出現(xiàn)，則置Sk +1= Sk tk/xk,k+1=ktk/xk，k=k+1，然后轉(zhuǎn)步2;步步5 算法停止，S的最一般合一不存在。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.16 求公式集S=P(a,x,f(g(y),P(z,h(z,u),f(u)的最一般合一。 解解 k=0： S0=S, 0=,S0不是單元素集，求得D0=a,z，其中z是變元，且不在a中出現(xiàn)，所以有 1=0a/z=a/z=a/zS1=S0a/z=P(a,x,f(g(y),P(a,h(a,u),f(u) k=1: S1不是單元素集，求得D1=x,h(a,u)， 第第5 5章章 基于謂詞邏輯的

14、機(jī)器推理基于謂詞邏輯的機(jī)器推理 所以2=1h(a,u)/x=a/zh(a,u)/x=a/u,h(a,u)/xS2=S1h(a,u)/x=P(a,h(a,u),f(g(y),P(a,h(a,u),f(u)k=2:S2不是單元素集，D2=g(y),u，3=2g(y)/u=a/z,h(a,g(y)/x,g(y)/uS3=S2g(y)/u=P(a,h(a,g(y),f(g(y),P(a,h(a,g(y),f(g(y)=P(a,h(a,g(y),f(g(y)k=3:S3已是單元素集，所以3就是S的最一般合一。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.17 判定S=P(x,x)

15、,P(y,f(y)是否可合一？解解k=0:S0=S,0=,S0不是單元素集，D0=x,y1=0y/x=y/xS1=S0y/x=P(y,y),P(y,f(y)k=1:第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 S1不是單元素集，D1=y,f(y)，由于變元y在項f(y)中出現(xiàn)，所以算法停止，S不存在最一般合一。 從合一算法可以看出，一個公式集S的最一般合一可能是不唯一的，因為如果差異集Dk=ak,bk，且ak和bk都是個體變元，則下面兩種選擇都是合適的： k+1=kbk/ak或k+1=kak/bk第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定理定理3 （合一定

16、理）如果S是一個非空有限可合一的公式集，則合一算法總是在步2停止，且最后的k即是S的最一般合一。本定理說明任一非空有限可合一的公式集，一定存在最一般合一，而且用合一算法總能找到最一般合一，這個最一般合一也就是當(dāng)算法終止在步2時，最后的合一k。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 3.2.4 謂詞邏輯中的歸結(jié)原理謂詞邏輯中的歸結(jié)原理 定義定義12 設(shè)C1,C2是兩個無相同變元的子句，L1,L2分別是C1,C2中的兩個文字，如果L1和L2有最一般合一，則子句(C1-L1)(C2-L2)稱作C1和C2的二元歸結(jié)式(二元消解式)，C1和C2稱作歸結(jié)式的親本子句，L1和L2稱作消

17、解文字。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.18 設(shè)C1=P(x)Q(x),C2=P(a)R(y)，求C1,C2的歸結(jié)式。 解解 取L1=P(x),L2=P(a),則L1與L2的最一般合一=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) 所以，Q(a)R(y)是C1和C2的二元歸結(jié)式。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.19 設(shè)C1=P(x,y)Q(a),C2=Q(x)R(y),求C1,C2的歸結(jié)式。 解解 由于C1,C2

18、中都含有變元x,y，所以需先對其中一個進(jìn)行改名,方可歸結(jié)（歸結(jié)過程是顯然的，故從略）。還需說明的是，如果在參加歸結(jié)的子句內(nèi)部含有可合一的文字，則在進(jìn)行歸結(jié)之前，也應(yīng)對這些文字進(jìn)行合一，從而使子句達(dá)到最簡。例如，設(shè)有兩個子句： C1=P(x)P(f(a)Q(x) C2=P(y)R(b)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 可見,在C1中有可合一的文字P(x)與P(f(a)，那么，取替換=f(a)/x(這個替換也就是P(x)和P(f(a)的最一般合一)，則得 C1=P(f(a)Q(f(a) 現(xiàn)在再用C1與C2進(jìn)行歸結(jié)，從而得到C1與C2的歸結(jié)式 (f(a)R(b) 定義定義

19、13 如果子句C中，兩個或兩個以上的文字有一個最一般合一，則C稱為C的因子，如果C是單元子句，則C稱為C的單因子。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.20 設(shè)C=P(x)P(f(y)乛Q(x),令=f(y)/x，于是C=P(f(y)乛Q(f(y)是C的因子。 定義定義14 子句C1,C2的消解式，是下列二元消解式 之一： (1)C1和C2的二元消解式; (2)C1和C2的因子的二元消解式; (3)C1的因子和C2的二元消解式; (4)C1的因子和C2的因子的二元消解式。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 定理定理4 謂詞邏輯中的消

20、解式是它的親本子句的邏輯結(jié)果。(證明類似于定理2，故從略。) 由此定理我們即得謂詞邏輯中的推理規(guī)則： C1C2 (C1-L1)(C2-L2) 其中C1,C2是兩個無相同變元的子句，L1,L2分別是C1,C2中的文字，為L1與L2的最一般合一。此規(guī)則稱為謂詞邏輯中的消解原理（或歸結(jié)原理）。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.21 求證G是A1和A2的邏輯結(jié)果。A1: x(P(x)(Q(x)R(x)A2: x(P(x)S(x)G: x(S(x)R(x) 證證 我們用反證法，即證明A1A2乛G不可滿足。首先求得子句集S： 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于

21、謂詞邏輯的機(jī)器推理 (1)乛P(x)Q(x) (2)乛P(y)R(y) (3)P(a) (4)S(a) (5)乛S(z)乛R(z)(乛G) 然后應(yīng)用消解原理，得(6)R(a) (2),(3),1=a/y(7)乛R(a) (4),(5),2=a/z(8) (6),(7)所以S是不可滿足的，從而G是A1和A2的邏輯結(jié)果。 (A1) (A2) S第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.22 設(shè)已知：(1)能閱讀者是識字的；(2)海豚不識字；(3)有些海豚是很聰明的。試證明：有些聰明者并不能閱讀。證 首先，定義如下謂詞：R(x)：x能閱讀。L(x)：x識字。I(x)：x是

22、聰明的。D(x)：x是海豚。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 然后把上述各語句翻譯為謂詞公式：(1) x(R(x)L(x)(2) x(D(x)乛L(x) 已知條件(3) x(D(x)I(x)(4) x(I(x)乛R(x) 需證結(jié)論 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 求題設(shè)與結(jié)論否定的子句集，得(1)乛R(x)L(x)(2)乛D(y)乛L(y)(3)D(a)(4)I(a)(5)乛I(z)R(z)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 歸結(jié)得(6) R(a) (5)，(4)，a/z(7) L (a) (6)，(1)，a

23、/x(8) 乛D(a) (7), (2), a/y(9) (8), (3)這個歸結(jié)過程的演繹樹如圖32所示。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 由以上例子可以看出，謂詞邏輯中的消解原理也可以代替其他推理規(guī)則。 上面我們通過推導(dǎo)空子句，證明了子句集的不可滿足性，于是存在問題：對于任一不可滿足的子句集，是否都能通過歸結(jié)原理推出空子句呢？回答是肯定的。 定理定理5 （歸結(jié)原理的完備性定理）如果子句集S是不可滿足的，那么必存在一個由S推出空子句的消解序列。(該定理的證明要用到Herbrand定理，故從略。) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 圖5

24、-2 例3.22 歸結(jié)演繹樹 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 歸結(jié)原理除了能用于對已知結(jié)果的證明外，還能用于對未知結(jié)果的求解，即能求出問題的答案來。請看下例。 例例3.23 已知: (1)如果x和y是同班同學(xué)，則x的老師也是y的老師。 (2)王先生是小李的老師。 (3)小李和小張是同班同學(xué)。 問：小張的老師是誰？ 5.3 應(yīng)用歸結(jié)原理求取問題答案應(yīng)用歸結(jié)原理求取問題答案第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 解解 設(shè)謂詞T(x,y)表示x是y的老師，C(x,y)表示x與y是同班同學(xué)，則已知可表示成如下的謂詞公式： F1: x y z(C(x,

25、y)T(z,x)T(z,y) F2:T(Wang,Li) F3:C(Li,Zhang) 為了得到問題的答案，我們先證明小張的老師是存在的，即證明公式： G: x T(x,Zhang) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 于是，求F1F2F3 G的子句集如下:(1) C(x,y) T(z,x)T(z,y)(2)T(Wang,Li)(3)C(Li,Zhang)(4) T(u,Zhang)歸結(jié)演繹，得(5) C(Li,y)T(Wang,y) 由(1),(2),Wang/z,Li/x(6) C(Li,Zhang) 由(4),(5),Wang/u,Zhang/y(7) 由(3)

26、,(6)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 這說明，小張的老師確實是存在的。那么，為了找到這位老師，我們給原來的求證謂詞的子句再增加一個謂詞ANS(u)。于是，得到 (4) T(u,Zhang)ANS(u)現(xiàn)在，我們用(4)代替(4)，重新進(jìn)行歸結(jié)，則得 (5) C(Li,y)T(Wang,y) 由(1)(2) (6) C(Li,Zhang)ANS(Wang) 由(4)(5) (7)ANS(Wang) 由(3)(6) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 可以看出，歸結(jié)到這一步，求證的目標(biāo)謂詞已被消去，即求證已成功，但還留下了謂詞ANS(Wan

27、g)。由于該謂詞中原先的變元與目標(biāo)謂詞T(u,Zhang)中的一致，所以，其中的Wang也就是變元u的值。這樣，我們就求得了小張的老師也是王老師。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 上例雖然是一個很簡單的問題，但它給了我們一個利用歸結(jié)原理求取問題答案的方法，那就是：先為待求解的問題找一個合適的求證目標(biāo)謂詞；再給增配（以析取形式）一個輔助謂詞，且該輔助謂詞中的變元必須與對應(yīng)目標(biāo)謂詞中的變元完全一致；然后進(jìn)行歸結(jié)，當(dāng)某一步的歸結(jié)式剛好只剩下輔助謂詞時，輔助謂詞中原變元位置上的項（一般是常量）就是所求的問題答案。需說明的是，輔助謂詞（如此題中的ANS）是一個形式謂詞，其作用

28、僅是提取問題的答案，因而也可取其他謂詞名。有些文獻(xiàn)中就用需求證的目標(biāo)謂詞。如對上例，就取T(u,Zhang)為輔助謂詞。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.24 設(shè)有如下關(guān)系:(1)如果x是y的父親，y又是z的父親，則x是z的祖父。(2)老李是大李的父親。(3)大李是小李的父親。問：上述人員中誰和誰是祖孫關(guān)系？解 先把上述前提中的三個命題符號化為謂詞公式：F1: x y z(F(x,y)F(y,z)G(x,z)F2: F(Lao,Da)F3: F(Da,Xiao) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 并求其子句集如下:(1)乛 F(x

29、,y)乛 F(y,z)G(x,z)(2)F (Lao,Da)(3)F (Da,Xiao)設(shè)求證的公式為G: x yG(x,y) (即存在x和y，x是y的祖父) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 把其否定化為子句形式再析取一個輔助謂詞GA(x,y)，得 (4)乛G(u,v)GA(u,v) 對(1)(4)進(jìn)行歸結(jié),得 (5)乛F(Da,z)G(Lao,z) (1),(2),Lao/x,Da/y (6)G(Lao,Xiao) (3),(5),Xiao/z (7)GA(Lao,Xiao) (4),(6),Lao/u,Xiao/v 所以，上述人員中，老李是小李的祖父。第第5

30、5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.4.1 問題的提出問題的提出 前面我們介紹了歸結(jié)原理及其應(yīng)用，但前面的歸結(jié)推理都是用人工實現(xiàn)的。而人們研究歸結(jié)推理的目的主要是為了更好地實現(xiàn)機(jī)器推理，或者說自動推理。那么，現(xiàn)在就存在問題：歸結(jié)原理如何在機(jī)器上實現(xiàn)？把歸結(jié)原理在機(jī)器上實現(xiàn)，就意味著要把歸結(jié)原理用算法表示，然后編制程序，在計算機(jī)上運行。下面我們給出一個實現(xiàn)歸結(jié)原理的一般性算法： 5.4 歸結(jié)策略歸結(jié)策略第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 步1 將子句集S置入CLAUSES表； 步2 若空子句NIL在CLAUSES中，則歸結(jié)成功，結(jié)束。 步3 若CL

31、AUSES表中存在可歸結(jié)的子句對，則歸結(jié)之，并將歸結(jié)式并入CLAUSES表，轉(zhuǎn)步2； 步4 歸結(jié)失敗，退出。 可以看出，這個算法并不復(fù)雜，但問題是在其步3中應(yīng)該以什么樣的次序從已給的子句集S出發(fā)尋找可歸結(jié)的子句對而進(jìn)行歸結(jié)呢？第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 一種簡單而直接的想法就是逐個考察CLAUSES表中的子句，窮舉式地進(jìn)行歸結(jié)?？刹捎眠@樣的具體作法：第一輪歸結(jié)先讓CLAUSES表(即原子句集S)中的子句兩兩見面進(jìn)行歸結(jié)，將產(chǎn)生的歸結(jié)式集合記為S1，再將S1并入CLAUSES得CLAUSESSS1；下一輪歸結(jié)時，又讓新的CLAUSES即SS1與S1中的子句互相見

32、面進(jìn)行歸結(jié)，并把產(chǎn)生的歸結(jié)式集合記為S2，再將S2并入CLAUSES；再一輪歸結(jié)時，又讓SS1S2與S2中的子句進(jìn)行歸結(jié)如此進(jìn)行，直到某一個Sk中出現(xiàn)空子句為止。下面我們舉例。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.25 設(shè)有如下的子句集S，我們用上述的窮舉算法歸結(jié)如下： S: (1)PQ (2)乛PQ (3)P乛Q (4)乛P乛Q S1:(5)Q (1),(2) (6)P (1),(3) (7)Q乛Q (1),(4) (8)P乛P (1),(4) (9)Q乛Q (2),(3) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (10)P乛P (2)

33、,(3) (11)乛P (2),(4) (12)乛Q (3),(4)S2:(13)PQ (1),(7) (14)PQ (1),(8) (15)PQ (1),(9) (16)PQ (1),(10) (17)Q (1),(11) (18)P (1),(12) (19)Q (2),(6) (20)乛PQ (2),(7)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (21)乛PQ (2),(8)(22)乛PQ (2),(9)(23)乛PQ (2),(10)(24)乛P (2),(12)(25)P (3),(5)(26)P乛Q (3),(7)(27)P乛Q (3),(8)(28)P乛Q

34、(3),(9)(29)P乛Q (3),(10)(30)乛Q (3),(11)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (31)乛P (4),(5)(32)乛Q (4),(6)(33)乛P乛Q (4),(7)(34)乛P乛Q (4),(8)(35)乛P乛Q (4),(9)(36)乛P乛Q (4),(10)(37)Q (5),(7)(38)Q (5),(9)(39) (5),(12)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 可以看出，這個歸結(jié)方法無任何技巧可言，只是一味地窮舉式歸結(jié)。因而對于如此簡單的問題，計算機(jī)推導(dǎo)了35步，即產(chǎn)生35個歸結(jié)式，才導(dǎo)出了空子

35、句。那么，對于一個規(guī)模較大的實際問題，其時空開銷就可想而知了。事實上，這種方法一般會產(chǎn)生許多無用的子句。這樣，隨著歸結(jié)的進(jìn)行，CLAUSES表將會越來越龐大，以至于機(jī)器不能容納。同時，歸結(jié)的時間消耗也是一個嚴(yán)重問題。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.4.2 幾種常用的歸結(jié)策略幾種常用的歸結(jié)策略 1.刪除策略刪除策略 定義 設(shè)C1,C2是兩個子句，若存在替換，使得C1C2，則稱子句C1類含C2。 例如： P(x)類含P(a)Q(y) (只需取=a/x) Q(y)類含P(x)Q(y) (=) P(x)類含P(x),P(x)類含P(a),P類含P,P類含PR P(a

36、,x)P(y,b)類含P(a,b) (取=b/x,a/y) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 刪除策略： 在歸結(jié)過程中可隨時刪除以下子句： (1)含有純文字的子句； (2)含有永真式的子句； (3)被子句集中別的子句類含的子句。 所謂純文字，是指那些在子句集中無補(bǔ)的文字。例如下面的子句集 P(x)Q(x,y)R(x),P(a)Q(u,v),Q(b,z),P(w)中的文字R(x)就是一個純文字。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 刪除含有純文字的子句，是因為在歸結(jié)時純文字永遠(yuǎn)不會被消去，因而用包含它的子句進(jìn)行歸結(jié)不可能得到空子句。刪除永真式

37、是因為永真式對子句集的不可滿足性不起任何作用。刪除被類含的子句是因為被類含子句被類含它的子句所邏輯蘊(yùn)含，故它已是多余的。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.26 我們在例3.25中使用刪除策略?？梢钥闯觯@時原歸結(jié)過程中產(chǎn)生的有些歸結(jié)式是永真式（如(7)、(8)、(9)、(10)），有些被前面已有的子句所類含（如(17)、(18)等，重復(fù)出現(xiàn)可認(rèn)為是一種類含），因此，它們可被立即刪除。這樣就導(dǎo)致它們的后裔將不可能出現(xiàn)。于是，歸結(jié)步驟可簡化為 (1)PQ (2)乛PQ (3)P乛Q (4)乛P乛Q第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (5

38、)Q (1),(2)(6)P (1),(3)(7)乛P (2),(4)(8)乛Q (3),(4)(9) (5),(8)其實，上述歸結(jié)還可以進(jìn)一步簡化為(5)Q (1),(2)(6)乛Q (3),(4)(7) (5),(6) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例3.27 對下面的子句集S，我們用寬度優(yōu)先策略與刪除策略相結(jié)合的方法進(jìn)行消解。 S: (1)P(x)Q(x)乛R(x) (2)乛Q(a) (3)乛R(a)Q(a) (4)P(y) (5)乛P(z)R(z)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 可以看出，(4)類含了(1)，所以先將(1)

39、刪除。于是，剩下的四個子句歸結(jié)得 S1: (6)乛R(a) (2),(3) (7)乛P(a)Q(a) (3),(5),a/z (8)R(z) (4),(5),z/y第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (6)出現(xiàn)后(3)可被刪除，所以，第二輪歸結(jié)在(2)、(4)、(5)、(6)、(7)、(8)間進(jìn)行。其中(2)、(4)、(5)間的歸結(jié)不必再重做，于是得 S2: (9)乛P(a) (2),(7) (10)Q(a) (4),(7),a/y (11)乛P(a) (5),(6),a/z (12) (6),(8),a/z第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理

40、 刪除策略有如下特點： 刪除策略的思想是及早刪除無用子句，以避免無效歸結(jié)，縮小搜索規(guī)模；并盡量使歸結(jié)式朝“小”（即元數(shù)少）方向發(fā)展。從而盡快導(dǎo)出空子句。 刪除策略是完備的。即對于不可滿足的子句集，使用刪除策略進(jìn)行歸結(jié)，最終必導(dǎo)出空子句。 定義 一個歸結(jié)策略是完備的，如果對于不可滿足的子句集，使用該策略進(jìn)行歸結(jié)，最終必導(dǎo)出空子句。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 2.支持集策略支持集策略 支持集策略：每次歸結(jié)時，兩個親本子句中至少要有一個是目標(biāo)公式否定的子句或其后裔。這里的目標(biāo)公式否定的子句集即為支持集。 例例5.28 設(shè)有子句集 S=乛I(x)R(x),I(a),乛

41、R(y)乛L(y),L(a) 其中子句I(x)R(x)是目標(biāo)公式否定的子句。 我們用支持集策略歸結(jié)如下： S:(1)乛I(x)R(x) (2)I(a) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 (3)乛R(y)乛L(y) (4)L(a) S1:(5)R(a) 由(1),(2),a/x (6)乛I(x)乛L(x) 由(1),(3),x/y S2:(7)乛L(a) 由(5),(3),a/y (8)乛L(a) 由(6),(2),a/x (9)乛I(a) 由(6),(4),a/x (10) 由(7),(4)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 支持集策略有如

42、下特點： 這種策略的思想是盡量避免在可滿足的子句集中做歸結(jié)，因為從中導(dǎo)不出空子句。而求證公式的前提通常是一致的，所以，支持集策略要求歸結(jié)時從目標(biāo)公式否定的子句出發(fā)進(jìn)行歸結(jié)。所以，支持集策略實際是一種目標(biāo)制導(dǎo)的反向推理。 支持集策略是完備的。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 3.線性歸結(jié)策略線性歸結(jié)策略 線性歸結(jié)策略：在歸結(jié)過程中，除第一次歸結(jié)可都用給定的子句集S中的子句外，其后的各次歸結(jié)則至少要有一個親本子句是上次歸結(jié)的結(jié)果。線性歸結(jié)的歸結(jié)演繹樹如圖53所示，其中C0,B0必為S中的子句， C0稱為線性歸結(jié)的頂子句； C0,C1,C2,Cn-1稱為線性歸結(jié)的中央子

43、句；B1,B2,Bn-1稱為邊子句，它們或為S中的子句，或為C1,C2, Cn-1中之一。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 圖53 線性歸結(jié)演繹樹 圖54 例3.29歸結(jié)演繹樹 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例5.29 對例5.28中的子句集，我們用線性歸結(jié)策略歸結(jié)。 (1)乛I(x)R(x) (2)I(a) (3)乛R(y)L(y) (4) L(a) (5) R(a) 由(1)(2),a/x (6)乛L(a) 由(5)(3),a/y (7) 由(6)(4) 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 其歸結(jié)反演樹如

44、圖54所示。 線性歸結(jié)策略的特點是：不僅它本身是完備的，高效的，而且還與許多別的策略兼容。例如在線性歸結(jié)中可同時采用支持集策略或輸入策略。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 4.輸入歸結(jié)策略輸入歸結(jié)策略 輸入歸結(jié)策略：每次參加歸結(jié)的兩個親本子句，必須至少有一個是初始子句集S中的子句?？梢钥闯觯?.29中的歸結(jié)過程也可看作是運用了輸入策略。輸入歸結(jié)策略的特點是： 輸入歸結(jié)策略實際是一種自底向上的推理，它有相當(dāng)高的效率。 輸入歸結(jié)是不完備的。例如子句集 S=PQ,乛PQ,P乛Q,P乛Q 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 是不可滿足的，用輸入歸

45、結(jié)都不能導(dǎo)出空子句，因為最后導(dǎo)出的子句必定都是單文字子句，它們不可能在S中。 輸入歸結(jié)往往同線性歸結(jié)配合使用，組成所謂線性輸入歸結(jié)策略。當(dāng)然，進(jìn)一步還可以與支持集策略結(jié)合。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 6.祖先過濾形策略祖先過濾形策略 祖先過濾形策略：參加歸結(jié)的兩個子句，要么至少有一個是初始子句集中的子句；要么一個是另一個的祖先（或者說一個是另一個的后裔）。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例例5.30 設(shè)有子句集S=乛P(x)Q(x),乛P(y)乛Q(y),P(u)Q(u),P(t)乛Q(t) 我們用祖先過濾形策略進(jìn)行歸結(jié)，過程

46、如圖55所示。其中最后歸結(jié)出空子句的兩個子句P(x)與P(u)，前者是后者的祖先。可以看出，祖先過濾形策略也可看作是線性輸入策略的改進(jìn)。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 圖55 例5.30歸結(jié)演繹樹 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 祖先過濾形策略的特點是：祖先過濾形策略也可看作是線性輸入策略的改進(jìn)。 祖先過濾形策略是完備的。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.4.3 歸結(jié)策略的類型歸結(jié)策略的類型 上面我們介紹了一些常用的歸結(jié)策略。除此而外，人們還提出了許多別的策略，如鎖歸結(jié)、語義歸結(jié)、加權(quán)策略、模型策略等

47、。鎖歸結(jié)的思想是：用數(shù)字1,2,3,對各子句中的文字進(jìn)行編號，使互不相同的文字或相同文字的不同出現(xiàn)具有不同的編號，這種編號就稱為文字的鎖，如1P3Q和5P9P中的1,3,5,9就都是鎖。這樣，歸結(jié)就可用鎖來控制。具體做法是：每次歸結(jié)，參加歸結(jié)的文字必須分別是所在子句中編號最小者。例如，有子句1P2Q和3P4Q，則只能對P、P作歸結(jié)。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 語義歸結(jié)的基本思想是將子句集S中的子句分成兩組，只考慮組間子句的歸結(jié)。加權(quán)策略是對子句或其中的項賦予相應(yīng)的權(quán)值，以反映子句或項在實際問題中的某種程度，這樣，歸結(jié)就可用權(quán)值來控制。如給出某種順序或限制。雖然

48、歸結(jié)策略很多，但歸納起來，大致可以分為三類： (1)簡化性策略。 (2)限制性策略。 (3)有序性策略。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 有了歸結(jié)策略后，本節(jié)開始所給的歸結(jié)反演一般算法可改為： 步1 將子句集S置入CLAUSES表； 步2 若空子句NIL在CLAUSES中，則歸結(jié)成功，結(jié)束。 步3 按某種策略在CLAUSES表中尋找可歸結(jié)的子句對，若存在則歸結(jié)之，并將歸結(jié)式并入CLAUSES表，轉(zhuǎn)步2； 步4 歸結(jié)失敗，退出。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.5 歸結(jié)反演程序舉例歸結(jié)反演程序舉例 下面我們給出一個可用于命題邏輯歸結(jié)反

49、演的PROLOG示例程序。 prove(F,S):-union(F,S,SY),proof(SY). union(,Y,Y). union(X|XR,Y,Z):-member(X,Y),!,union(XR,Y,Z). union(X|XR,Y,X|ZR):-union(XR,Y,ZR). 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 proof(SH|ST):-resolution(SH,ST,),!.proof(SH|ST):-resolution(SH,ST,NF),proof(NF,SH|ST).resolution(SH,STH|ST,NF):-resolve(SH,

50、STH,NF1),NF1=SH,!,resolution(SH,ST,NF).resolution(SH,STH|ST,NF):-resolve(SH,STH,NF),print(SH,STH,NF). resolve(,-,):-!.resolve(F|FR,SF,FR):-not(F=no),invert(F,IF),IF=SF,!.resolve(F|FR,SF,NF):not(F=no),invert(F,IF),member(IF,SF),!,第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 pack(F,FR,SF,NF).resolve(F|FR,SF,NF):-no

51、t(F=no),!,resolve(FR,SF,NF1),pack(,F,NF1,NF).resolve(F,SF,):-invert(F,IF),IF=SF,!.resolve(F,SF,NF):-invert(F,IF),member(IF,SF),!,pack(F,SF,NF).resolve(F,-,F). invert(X,no,X):-atom(X). 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 invert(no,X,X):-atom(X). member(X,X|-):-!.member(X,-|Y):-member(X,Y). pack(A,X,Y,Z):-

52、combine(A,X,Y,Z|),!.pack(A,X,Y,Z):-combine(A,X,Y,Z). combine(A,X,Y,Z): -union(X,Y,Z1),delete(A,Z1,Z2),invert(A,IA),delete(IA,Z2,Z). delete(-,).delete(E,E|ER,R):-!,delete(E,ER,R).delete(E,X|XR,X|R):-delete(E,XR,R). print(F,S,R):-write(F),write(,),write(S),write(),write(R),nl.第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯

53、的機(jī)器推理 該程序把子句用表表示。例如：子句PQ，則表示為：not,p,q。子句集用子句表表示。例如：子句集乛PQ,RS,U，則表示為 not,p,q,r,s,u第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 該程序的目標(biāo)子句是prove(F,S)，其中S為前提，F(xiàn) 為 要 證 明 的 結(jié) 論 的 否 定 。 程 序 運 行 時 ， 謂 詞union(F,S,FS)首先把待證結(jié)論的否定子句F與前提子句S合并為FS。接著，謂詞proof(FS)對子句集FS進(jìn)行歸結(jié)反演，試圖推出空子句。proof又調(diào)用謂詞resolution進(jìn)行歸結(jié)。proof的第一個子句是歸結(jié)反演的終結(jié)條件；第二

54、個子句是歸結(jié)反演的遞歸操作。第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 resolution(SH,ST,NF)謂詞實現(xiàn)具體的歸結(jié)操作。其中SH是從子句集FS中分離出的一個子句，它作為一個雙親子句；ST為去掉SH后的子句集；NF是SH與ST中子句產(chǎn)生的歸結(jié)式。 resolution的第一個子句處理ST子句集中的第一個子句STH不能與SH歸結(jié)的情況，將引起resolution的遞歸操作。 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.6 Horn子句歸結(jié)與邏輯程序子句歸結(jié)與邏輯程序 5.6.1 子句的蘊(yùn)含表示形式子句的蘊(yùn)含表示形式 我們知道，原子公式及其否定

55、稱為文字，現(xiàn)在我們把前者稱為正文字，后者稱為負(fù)文字。例如子句P(x)Q(x,y)中P(x)為正文字，Q(x,y)為負(fù)文字。我們還知道，子句是若干文字的析取，析取詞又滿足交換律，所以對于任一個子句我們總可以將其表示成如下形式： 乛Q1乛QnP1Pm 第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 其中Pi,乛Qj皆為文字?？梢钥闯觯?31)式進(jìn)一步可變形為 Q1Q2QnP1P2Pm (32) (32)式為一個蘊(yùn)含式，如果我們約定蘊(yùn)含式前件的文字之間恒為合取關(guān)系，而蘊(yùn)含式后件的文字恒為析取關(guān)系，那么(32)式又可以改寫為 Q1,Q2,QnP1,P2,Pm (33) 由于技術(shù)上的原因，

56、我們又將(33)式改寫為 P1,P2,PmQ1,Q2,Qn (34)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 作為特殊情形，當(dāng)m=0時(34)式變?yōu)?Q1,Q2,Qn (34) 它相當(dāng)于(Q1Q2Qn)；當(dāng)n=0時，(34)式變?yōu)?P1,P2,Pm (34) 它相當(dāng)于P1P2Pm。 這樣，對于任一子句，我們總可以把它表示成(34)式的形式。子句的這種表示形式稱為子句的蘊(yùn)含表示形式。例如，子句P(x)Q(x,y)R(y)的蘊(yùn)含表示形式為 Q(x,y)P(x),R(y)第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 例如，子句Q1(x),Q2(x)P1(x),P2

57、(x)和P1(y)R1(y),R2(y)的歸結(jié)式為 Q1(x),Q2(x)R1(x),R2(x),P2(x) 一般地，這種蘊(yùn)含型子句的歸結(jié)過程可表示如下:設(shè)子句 C：P1,PmQ1,Qn 和 C：P1,PsQ1,Qt 中有Pi與Qj（或Qi與Pj）可合一，為它們的mgu，則C與C的歸結(jié)式為第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 P1,P i-1,P i+1,Pm,P1,PsQ1,Qn,Q1,Qj-1,Qj+1,Qt或P1,Pm,P1,Pj-1,Pj+1,PsQ1,Q i-1,Q i+1,Qn,Q1,Qt第第5 5章章 基于謂詞邏輯的機(jī)器推理基于謂詞邏輯的機(jī)器推理 5.6.2 Horn子句與邏輯程序子句與邏輯程序 定義1 至多含有一個正文字的子句稱為Horn（有些文獻(xiàn)中譯為“霍恩”）子句。（因邏輯學(xué)家AlfredHorn首先研究它而得名。）由定義，蘊(yùn)含型Horn子句有下列三種： (1)PQ1,Q2,Qm 稱為條件子句,P