人工智能第五章

人工智能第五章本章內(nèi)容簡介合一及合一算法正向演繹系統(tǒng)反向演繹系統(tǒng)25.1歸結(jié)反演系統(tǒng)5.1.1謂詞演算基礎(chǔ)--一階謂詞邏輯

1.永真性和可滿足性如果一個公式對所有的解釋都有值T，則稱它是永真的。例如，用真值表可以證明：P(A)[P(A)∨P(B)]是永真的。設(shè)I是一個解釋，使集合S中所有的公式均取值T，則稱I滿足S。

如果每一個適用于合式公式集合S的解釋也適用于合式公式X，則稱X邏輯上遵從公式集S。3例：S={P(A),┐P(A)∨P(B)}I1 P(A)=T,P(B)=T--I1適用于SI2 P(A)=F,P(B)=T--I2不適用于S

一個公式X邏輯上遵從公式集S----每個滿足S的解釋也滿足X.例：X--Q(A) S--{P(A).P(A)Q(A)}4定理：若S是合式公式F的S-標準形之子句集，則F為永假的充要條件是S為不可滿足的。5

2.

推理規(guī)則、定理和證明推理：從已知合式公式推理產(chǎn)生的新的合式公式。證明：推理過程中所用的規(guī)則序列。推理規(guī)則：用于某些合式公式,以產(chǎn)生新的合式公式。假言推理:W1,W1W2->W2 modusponens全稱消去推理:(x)W(x)->W(A) universalinstantiation63.子句歸結(jié)原理是由兩個子句推導出新的子句，需要將一般化的表達式化為標準式。因此首先說明如何把任一合式公式轉(zhuǎn)換成一個子句集。7例：(x){P(x){(y)[P(y)P(f(x,y))]∧┐(y)[Q(x,y)P(y)]}}轉(zhuǎn)化成子句的過程如下：(1)消除蘊含符號PQ->┐P∨Q(x){┐P(x)∨{(y)[┐P(y)∨P(f(x,y))]∧┐(y)[┐Q(x,y)∨P(y)]}}8(2)把┐移至每個謂詞符號前 利用┐(z)X(z)(z)[┐X(z)]┐(X1∨X2)┐X1∧┐X2有┐(y)[┐Q(x,y)∨P(y)]->(y)[┐[┐Q(x,y)∨P(y)]]->(y)[Q(x,y)∧┐P(y)]上式成為(x){┐P(x)∨{(y)[┐P(y)∨P(f(x,y))]

∧(y)[Q(x,y)∧┐P(y)]}}9(3)變量標準化--使每個量詞有不同的變量(x){┐P(x)V{(y)[┐P(y)VP(f(x,y))] (w)[Q(x,w)┐P(w)]}}(4)消除存在量詞

(y)[(x)P(x,y)]->(y)P[g(y),y)] 函數(shù)g(y)稱為skolem函數(shù)。g是原公式中沒有的符號(x)P(x)->P(A)A是原公式中沒有的符號公式成為(x){┐P(x)V{(y)[┐P(y)VP(f(x,y))] [Q(x,g(x))┐P(g(x))]}}10(5)化成前束形--把所有全稱量詞移到公式的前部。前束形的形式：x1x2...xn無量詞公式 前綴 母式公式成為(x)(y){┐P(x)V{[┐P(y)VP(f(x,y))] [Q(x,g(x))┐P(g(x))]}}11(6)把母式化成合取范式--一串用連接起來的子句 X1V(X2X3)->(X1VX2)(X1VX3)公式成為(x)(y){[┐P(x)V┐P(y)VP(f(x,y))] {┐P(x)V[Q(x,g(x))┐P(g(x))]}}(x)(y){[┐P(x)V┐P(y)VP(f(x,y))][┐P(x)VQ(x,g(x))][┐P(x)V┐P(g(x))]}12(7)消除全稱量詞形式上消去全稱量詞，但母式中的變量仍然是全稱量詞量化的變量，且作用范圍不變。(8)消除符號--將母式變成一組子句(X1X2)->{x1,X2}公式[┐P(x)V┐P(y)VP(f(x,y))][┐P(x)VQ(x,g(x))][┐P(x)V┐P(g(x))]成為 ┐P(x)V┐P(y)VP(f(x,y)) ┐P(x)VQ(x,g(x)) ┐P(x)V┐P(g(x))13

(9)重新命名變量--使每個子句中的變量符號不同這是因為(x)[P(x)Q(x)] [(x)P(x)(y)Q(y)]例中 ┐P(x1)V┐P(y)VP(f(x1,y))┐P(x2)VQ(x2,g(x2))┐P(x3)V┐P(g(x3))144.合一合一:尋找項對變量的置換而使表達式一致的過程。置換:一個置換是形如s={t1/v1,t2/v2,...,tn/vn}的有限集合,其中vi是變量符號,ti是不同于vi的項,且有vi≠vj,當i≠j時,稱ti為vi置換的分子,vi為置換的分母.

置換:變量<-項15例:置換的結(jié)果表達式P[x,f(y),B]通過不同的置換得到不同的例:P[z,f(w),B]s1={z/x,w/y}變量<-變量P[x,f(A),B]s2={A/y}變量<-常量P[g(z),f(y),B]s3={g(z)/x}變量<-函數(shù)P[C,f(A),B]s4={C/x,A/y}變量<-常量16Es：用置換s作用于表達式E所得到的例,如:P[z,f(w),B]=P[x,f(y),B]s117

合成：當用兩個置換s1和s2依次作用于一個表達式時，可以將兩個置換s1和s2組合為一個置換稱為s1與s2的合成，記為s1s2 {g(x,y)/z}{A/x,B/y,C/w,D/z}=？？ (1)把s2作用于s1 g(A,B)/z (2)把s1中所沒有的那些s2中的對加入到s1 A/x,B/y,C/w{g(A,B)/z,A/x,B/y,C/w}18

置換的性質(zhì):(1)(Es1)s2=E(s1s2)(2)(s1s2)s3=s1(s2s3) 結(jié)合律(3)交換律一般不成立如{A/x,B/y,C/w,D/z}{g(x,y)/z}=？？{A/x,B/y,C/w,D/z}{g(A,B)/z,A/x,B/y,C/w}19

{Ei}s：把置換s作用于集合{Ei}中的每個表達式得到的例的集。{Ei}是可合一的：ifsst.E1s=E2s=E3s=…,then{Ei}是可合一的,s是{Ei}的合一者。例如:s={A/x,B/y} {P[x,f(y),B],P[x,f(B),B]}s ={P[A,f(B),B],P[A,f(B),B]}合一的目的是促成互補對!20

最簡合一者mgu(mostgeneralunifier):ifs(s是{Ei}的合一者),s'st.{Ei}s={Ei}gs',theng為{Ei}的mgu。mgu的唯一性:除變量字母可以不同外,mgu是唯一的。上例的mgu應為{B/y}。21

例子：表達式集合{P(x),P(f(y)}是可合一的，mgu={f(y)/x}，對任一合一s={f(a)/x，a/y}都有替換r={a/y},使得s={f(y)/x}{a/y}22

下面給出一個合一程序UNIFY,它使用表結(jié)構(gòu)表達式 P(x,f(A,y))-->(Px(fAy))可以證明，UNIFY找到的是mgu。23

遞歸程序UNIFY(E1,E2)1.ifatom(E2)then交換E1,E22.ifatom(E1)then3.begin4.ifE1=E2,thenreturnNIL5.ifE1為變量then6.begin7.ifE2中有E1,thenreturnFAIL//xf(x)8.elsereturn{E2/E1}9.end10.ifE2為變量thenreturn{E1/E2}11.elsereturnFAIL12.end //E1和E2都是表2413.F1(CARE1),T1(CDRE1) //CAR->FIRST14.F2(CARE2),T2(CDRE2) //CDR->TAIL15.Z1UNIFY(F1,F2)16.ifZ1=FAILthenreturnFAIL17.G1T1.Z1 //Z1作用于T118.G2T2.Z1 //Z1作用于T219.Z2UNIFY(G1,G2)20.ifZ2=FAILthenreturnFAIL21.returnZ1.Z2 //返回Z1,Z2的合成25

步1-12處理遞歸到底的情況，也就是E1和E2有一個是原子的情況。步13-21處理E1和E2都是表的情況。

例：P[f(x),y,g(y)],P[f(x),z,g(x)]化為LISP形式：E1=(P(fx)y(gy))E2=(P(fx)z(gx))26E1,E2P,P.((fx)y(gy)),((fx)z(gx)){}(fx),(fx).(y(gy)),(z(gx))f,f.(x),(x)y,z.((gy)),((gx)){}x,x.NIL,NIL{y/z}(gy),(gx).NIL,NIL{}{}g,g.(y),(x){}{}y,x.NIL,NIL返回{y/z,y/x}{y/x}{}27合一算法差異集合:設(shè)W是非空表達式集合,W的差異集合是如下構(gòu)成的一個集合:首先找出W的所有表達式不是都相同的第一個符號,然后從W的每個表達式中抽出不相同的子表達式.所有這些子表達式組成的集合就是W的差異集合D.

28合一算法如果D中無變量符號,則W是不可合一的.W={P(f(x)),P(g(x))},則D={f(x),g(x)};如果D中只有一個元素,則W是不可合一的.W={P(x),P(x,y)},則D={y};如果D中有變量符號x和項t,且x出現(xiàn)在t中,則W是不可合一的.W={P(x),P(f(x))},則D={x,f(x)};29合一算法步驟1:置k=0,Wk=W,Ak=ε;步驟2:若Wk只有一個元素,則停止,Ak是W的mgu;否則找出Wk的差異集合Dk;步驟3:若Dk中存在元素vk和tk,其中vk是變量符號,并且不出現(xiàn)在tk中,則轉(zhuǎn)4;否則,算法停止,W是不可合一的;步驟4:令Ak+1=Ak.{tk/vk},Wk+1=Wk{tk/vk};步驟5:k=k+1,轉(zhuǎn)2;30例題1、D0={y,z},A1={y/z},W1={P[f(x),y,g(y)],P[f(x),y,g(x)]}2、D1={y,x},A2=A1{y/x}={y/z,y/x},W2={P[f(y),y,g(y)]}3、停止，mgu=A2={y/z,y/x}W={P[f(x),y,g(y)],P[f(x),z,g(x)]}31標準式的應用問題定理：若S是合式公式F的S標準形的子句集，則F為永假的充要條件是S為不可滿足的。32歸結(jié)反演歸結(jié)原理的基本思想:設(shè)法檢驗擴充的子句集Si是否含有空子句,若S集中存在空子句,則表明S為不可滿足的.若沒有空子句,則進一步用歸結(jié)法從S中導出S1,然后再檢驗S1是否有空子句(S1的不可滿足性等價于S的不可滿足性).這樣,歸結(jié)過程可以一直進行下去,這就是要通過歸結(jié)過程演繹出S的不可滿足性來,從而使定理得到證明.33

1.基子句的歸結(jié)基子句：沒有變量的子句稱為基子句。原理--設(shè)有兩個基子句 P1VP2V...VPn和┐P1VQ2V...VQm 其中所有的Pi和Qj都是不同的。從這兩個子句可以推論出一個新的子句，稱為它們的歸結(jié)式 P2VP3V...VPnVQ2V...VQm34證明：如果設(shè)P1為假，因為P1VP2V...VPn為真，故P2,...,Pn之中必有一個為真。如果設(shè)P1為真，則┐P1為假，因為┐P1VQ2V...VQm為真，Q2,...,Qm之中必有一個為真。不論哪種情況，都有P2VP3V...VPnVQ2V...VQm必為真。35

2.一般子句的歸結(jié)首先將給定的子句表示成文字的集 合 P1VP2V...VPn->{P1,P2,...,Pn}->{Pi}設(shè)有文字集{Li}和{Mi}，令{li}{Li}，{mi}{Mi}，({li}是{Li}的一個子集，{mi}是{Mi}的一個子集)，設(shè)s是{li}和{┐mi}的并集的mgu，則由{Li}和{Mi}可得出歸結(jié)式 {{Li}-{li}}s∨{{Mi}-{mi}}s歸結(jié)式不是唯一的。36例： P[x,f(A)]VP{x,f(y)]VQ(y)和 ┐P[z,f(A)]V┐Q(z)取 {li}={P[x,f(A)]} {mi}={┐P[z,f(A)]}，s={z/x}得 P[z,f(y)]V┐Q(z)VQ(y)取 {li}={P[x,f(A)],P{x,f(y)]}，{mi}={┐P[z,f(A)]}，s={z/x,A/y}得 Q(A)V┐Q(z)37

推論：子句集S={C1，C2，...，Cn}和子句集S1={C，C1，C2，...，Cn}的不可滿足性是等價的。S1是對S應用歸結(jié)法后推出的子句集。38

3.歸結(jié)反演為證明：公式集S->目標公式W(即子句W邏輯上遵從S)，方法為(1)將┐W加入到集合S。(2)將新的S轉(zhuǎn)換成一組子句，應用歸結(jié)原理推導出一個空子句。39歸結(jié)反演就是用歸結(jié)和反演實現(xiàn)定理的證明。因為空子句可以看成一個矛盾，顯然由P和┐P才能推導出一個空子句，因此集合S和┐W是矛盾的。也就是說，如果集合S中的合式公式全為真，則┐W必為假，因此W必為真。這與數(shù)學上的反證法類似，因此叫反演法。40例:已知(1)Whoevercanreadisliterate. (x)[R(x)L(x)]->{┐R(x)VL(x)}(2)Dolphinsarenotliterate. (y)[D(y)┐L(y)]->{┐D(y)V┐L(y)}(3)Somedolphinsareintelligent. (z)[D(z)I(z)]->{D(A)I(A)}->{D(A),I(A)}證明:(4)Somewhoareintelligentcannotread.G:(w)[I(w)┐R(w)]┐G:(w)[┐I(w)VR(w)]->{┐I(w)VR(w)}41子句集: {┐R(x)VL(x)} {┐D(y)V┐L(y)} {D(A),I(A)} {┐I(w)VR(w)}42

┐I(w)VR(w)I(A)R(A)43

┐I(w)VR(w)I(A)R(A)┐R(x)VL(x)L(A)44

┐I(w)VR(w)I(A)R(A)┐R(x)VL(x)L(A)┐D(y)V┐L(y)

┐D(A)45

┐I(w)VR(w)I(A)R(A)┐R(x)VL(x)L(A)┐D(y)V┐L(y)

┐D(A)D(A)反演樹46反演樹(只包括空子句及其祖先) --與或圖搜索的解圖導引圖(整個搜索樹) --與或圖搜索的搜索圖一個歸結(jié)反演可用導引圖中的反演樹表示。控制策略--生長引導圖直到產(chǎn)生一個反演樹為止。47過程RESOLUTION（1）CLAUSES=S（2）untilNIL∈CLAUSES，do（3）begin（4）在CLAUSES中選擇兩個不同的可歸結(jié)的子句Ci和Cj（5）計算Ci和Cj的歸結(jié)式rij（6）CLAUSES=CLAUSES∨{rij}（7）end485.1.3歸結(jié)反演的控制策略1、寬度優(yōu)先策略2、支持集策略歸結(jié)式的母式子句至少有一個是目標公式的否定及其后代3、單元優(yōu)先策略4、線性輸入形策略歸結(jié)式的母式子句至少有一個屬于基本集。5、祖先過濾形策略歸結(jié)式的母式子句至少有一個屬于基本集，或者是另一個母式子句的祖先。495.1.4從歸結(jié)反演中提取解答在定理證明系統(tǒng)中，有這樣一類問題，即目標公式中有存在量詞量化的變量，我們希望得到這個變量的一個例，這就需要在證明解序列的過程中提取這個解答。50某地被盜，公安局派出5個偵察員前往調(diào)查。經(jīng)過偵察，在研究案情時，偵察員A說：“趙與錢中至少有一人作案”；偵察員B說：“錢與孫中至少有一人作案”；偵察員C說：“孫與李中至少有一人作案”；偵察員D說：“趙與孫中至少有一人與此案無關(guān)”；偵察員E說：“錢與李中至少有一人與此案無關(guān)”；。如果這五個偵察員的話都是可信的，請問誰是嫌疑人呢？51第一步:將五位偵察員的話表示成謂詞公式，為此先定義謂詞。設(shè)謂詞P(x)表示是嫌疑人，根據(jù)偵察員的結(jié)論：A:P(zhao)∨P(qian)B:P(qian)∨P(sun)C:P(sun)∨P(li)D:～P(zhao)∨

～P(sun)E:～P(qian)∨

～P(li)第二步：將待求解的問題表示成謂詞。設(shè)y是盜竊嫌疑人，則問題的謂詞公式為P(y)，將其否定與ANSWER(y)析取～P(y)∨ANSWER(y)52第三步：求前提條件及～P(y)∨ANSWER(y)的子句集，并將各子句列在下面:(1)P(zhao)∨P(qian)(2)P(qian)∨P(sun)(3)P(sun)∨P(li)(4)～P(zhao)∨

～P(sun)(5)～P(qian)∨

～P(li)(6)～P(y)∨ANSWER(y)53第四步：應用歸結(jié)原理進行推理(7)P(qian)∨

～P(sun)(8)P(zhao)∨

～P(li)(9)P(qian)∨

～P(zhao)(10)P(sun)∨

～P(li)(11)～P(zhao)∨P(li)(12)P(sun)∨

～P(qian)(13)P(qian)(14)P(sun)(15)ANSWER(qian)(16)ANSWER(sun)所以，有兩個盜竊嫌疑人：錢和孫。54例1：事實:(1)FidogoeswhereverJohngoes. (x)[AT(JOHN,x)AT(FIDO,x)](2)Johnisatschool.AT(JOHN,SCHOOL)問題:(3)WhereisFido? G: (x)AT(FIDO,x)把三個合式公式轉(zhuǎn)換成子句： ┐AT(JOHN,x)VAT(FIDO,x)AT(JOHN,SCHOOL)┐G：(y)[┐AT(FIDO,y)]->┐AT(FIDO,y)55歸結(jié)法求解：

┐AT(FIDO,y)AT(FIDO,x)V┐AT(JOHN,x)x/y

┐AT(JOHN,x)

AT(JOHN,SCHOOL)SCHOOL/xNIL56(1)在目標公式的否定所形成的子句后，附加上該子句的否定。 ┐AT(FIDO,y)->┐AT(FIDO,y)VAT(FIDO,y)同語反復（重言式），即含有一個文字及其否定的子句(2)進行與上述反演樹同樣的歸結(jié)求解。為此，在生成反演樹時，對被合一的文字作上標記。 合一集：子句中被合一的文字集合。(3)把根結(jié)點的子句作為回答語句。57┐AT(FIDO,y)VAT(FIDO,y)AT(FIDO,x)V┐AT(JOHN,x)x/y

┐AT(JOHN,x)VAT(FIDO,x)AT(JOHN,SCHOOL)SCHOOL/xAT(FIDO,SCHOOL)修改證明樹58例3：目標公式包括全稱量詞事實：(1)(x)C(x,p(x)) ->C(x,p(x)) (2)(x)(y)[C(x,y)P(y,x)] -> ┐C(x,y)VP(y,x)->┐C(z,y)VP(y,z)問題：對任何一個x，誰是x的父輩？(3)(x)(y)P(y,x)否定：(x)(y)[┐P(y,x)] ->┐P(y,A) ->┐P(w.A)59先歸結(jié)求解：┐P(w,A)

┐C(z,y)VP(y,z)A/z,y/w

┐C(A,y)

C(x,p(x))A/x,p(A)/y反演樹同語反復：┐P(w,A)VP(w,A)60┐P(w,A)VP(w,A)┐C(z,y)VP(y,z)A/x,y/w

┐C(A,y)VP(y,A)C(x,p(x))A/x,p(A)/yP(p(A),A)修改的證明樹61事實上可以證明：

在問題提取過程中，用新變量代替來自目標公式否定式的子句中的Skolem函數(shù)是正確的。62回答提取過程可歸納如下：生成反演樹，并對樹中的合一集加以標記。對目標公式的否定式中出現(xiàn)的Skolem函數(shù)代以新變量。把目標公式的否定式化為重言式。仿照反演樹，生成修改證明樹（采用相應的合一集）。修改證明樹的根結(jié)點的子句即為回答子句。63

┐P(w,t)VP(w,t)┐C(z,y)VP(y,z)t/z,y/w

┐C(t,y)VP(y,t)C(x,p(x))t/x,p(t)/yP(p(t),t)上例的修改證明樹645.2基于規(guī)則的演繹系統(tǒng)┐A∧┐B→C┐A∧┐C→B┐B∧┐C→A┐A→B∨C┐B→A∨C┐C→A∨B與A∨B∨C等價浪費信息，降低效率65把上一節(jié)表示事實的合式公式分成事實與規(guī)則兩種類型，其中把具有蘊涵形式的合式公式稱為規(guī)則，事實由無蘊涵形式的表達式表示，目標就是由事實和規(guī)則證明目標公式。66把推導過程看做是一個產(chǎn)生式系統(tǒng)，把描述領(lǐng)域知識的邏輯語句分為兩類：一類是描述該領(lǐng)域的一般性規(guī)律的，轉(zhuǎn)換為產(chǎn)生式規(guī)則；另一類是描述為該領(lǐng)域的一個具體情況或狀態(tài)的，轉(zhuǎn)換成產(chǎn)生式系統(tǒng)的狀態(tài)描述。演繹系統(tǒng)就是根據(jù)這些事實和規(guī)則來證明一個目標公式。這種定理證明系統(tǒng)稱為直接系統(tǒng)，也叫基于規(guī)則的（直接證明）系統(tǒng)。675.2.1正向演繹系統(tǒng)1.事實表達式的與或形式 無蘊涵形式，或稱與或形式:(1)消除蘊涵符號(2)把┐符號移至每個謂詞符號前(3)變量標準化：使每個謂詞有不同的變量(4)消除存在量詞(5)轉(zhuǎn)換成前束式(6)消除全稱量詞(7)重新命名變量（使同一變量不出現(xiàn)在不同的主要合取式中）68前節(jié)所述的把合式公式轉(zhuǎn)換成子句的9個步驟中，第6步把母式轉(zhuǎn)換成合取范式和第8步把母式轉(zhuǎn)換成一組子句，這兩步不執(zhí)行。69例:(u)(v){Q(v,u)∧┐[[R(v)∨P(v)]∧S(u,v)]}移進┐:(u)(v){Q(v,u)∧[[┐R(v)∧┐P(v)]∨┐S(u,v)]}消除:(v){Q(v,A)∧[[┐R(v)∧┐P(v)]∨┐S(A,v)]}消除：Q(v,A)∧{┐R(v)∧┐P(v)]∨┐S(A,v)}重新命名變量：Q(w,A)∧{┐R(v)∧┐P(v)∨┐S(A,v)}70用與或圖表示事實表達式：用∧連接起來的k個子表達式用k個1-連接符連接到父結(jié)點。用∨連接起來的k個子表達式用1個k-連接符連接到父結(jié)點。71最初我們有事實表達式（A∨B）。因為我們不知道A或B哪個是真，所以可以試著首先假設(shè)A是真來證明，然后假設(shè)B是真來證明。如果兩個證明都成功，則我們得到一個確是根據(jù)析取式（A∨B）的一個證明。而A或B哪一個是真都無關(guān)緊要。72在圖中標有（A∨B）節(jié)點的兩個后裔是有一個2-連接符來連接的，因此這兩個后裔都必須出現(xiàn)在最后的解圖中。如果對節(jié)點n的一個解圖通過k-連接符包含有n的任一后裔，則解圖也必須包含通過這k-連接符的所有k個后裔?，F(xiàn)在我們就會明白使用k-連接符來分離事實中有關(guān)子表達式析取關(guān)系的直觀理由。73根結(jié)點 Q(w,A)∧{[┐R(v)∧┐P(v)]∨┐S(A,v)} Q(w,A)[┐R(v)∧┐P(v)]∨┐S(A,v)葉結(jié)點

┐R(v)∧┐P(v) ┐S(A,v)

┐R(v)┐P(v)與或圖表示的一個重要性質(zhì)是表達式本身所轉(zhuǎn)換出的一組子句可以從與或圖中讀出。例如上述事實表達式可分為三個子句：Q(w,A)┐S(A,v)∨┐R(v)┐S(A,v)∨┐P(v)74可見：一個與或圖表示的子句集就對應于在圖的文字結(jié)點上結(jié)束的解圖集。752.利用規(guī)則轉(zhuǎn)換與或圖規(guī)則形式：LW其中：(1)L是一個單一的文字，而W是任意的一個與或形式的表達式。正向演繹系統(tǒng)應用規(guī)則作用于事實表示的與或圖，改變與或圖的結(jié)構(gòu)，從而產(chǎn)生新的事實。76若有(L1∨L2)W，則可化為兩條規(guī)則：L1W和L2W。若有(L1∧L2)W，則可化為L1(L1W)，再為L1(┐L2∨W)。(2)L和W的所有變量都是全稱量化的。(3)各個規(guī)則中的變量都各不相同，而且規(guī)則中的變量和事實表達式中的變量也不同。77把規(guī)則轉(zhuǎn)換成要求的形式：例：(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)[┐P(x,y,f(x,y))]∨(u)Q(x,u)}轉(zhuǎn)換成前束式，消除全稱量詞：

┐P(x,y,f(x,y))∨Q(x,u)恢復蘊涵式： P(x,y,f(x,y))Q(x,u)78

用規(guī)則轉(zhuǎn)換與或圖例： 事實 [(P∨Q)∧R]∨[S∧(T∨U)] 規(guī)則 S(X∧Y)∨Z79

XY X∧YZ PQ STUP∨Q R S T∨U(P∨Q)∧R S∧(T∨U) [(P∨Q)∧R]∨[S∧(T∨U)]80規(guī)則的子句形式是

┐S∨[(X∧Y)∨Z]-> ┐S∨[(X∨Z)∧(Y∨Z)]-> ┐S∨X∨Z和┐S∨Y∨Z事實表達式中能夠與規(guī)則子句求解的子句為

S∨R 和 S∨P∨Q

應用歸結(jié)原理，可得出下列子句：

R∨X∨Z R∨Y∨Z

P∨Q∨X∨ZP∨Q∨Y∨Z81對結(jié)點S應用了一條規(guī)則后，還可對結(jié)點應用其它的規(guī)則。也就是說，規(guī)則可應用于圖中所有的文字結(jié)點。使用匹配弧使新的與或圖既可表示原來的與或表達式，也表示了新產(chǎn)生的與或表達式。823．用目標公式做結(jié)束條件目標公式采用文字的析取形式表示目標文字的結(jié)點稱為目標結(jié)點例：事實--A∨B 規(guī)則--A(C∧D) B(E∧G) 目標--C∨G∨F83 C 目標結(jié)點 GC D EGABAB A∨B規(guī)則--A(C∧D) B(E∧G)目標--C∨G∨F84結(jié)束條件：與或圖包括了一個在目標結(jié)點上結(jié)束的解圖。子句集（解圖集）： A∨B A∨E A∨G C∨B C∨E C∨G C∨G∨F D∨B D∨E D∨GC∨G雖然與目標公式不同，但比目標公式更一般。854．包括變量的表達式事實和規(guī)則---所有存在變量都被Skolem函數(shù)所替代，表達式中尚存的變量都被認為是全稱變量。目標---所有全稱變量都被Skolem函數(shù)所替代，存在量詞被去掉，表達式中尚存的變量都被認為是存在變量。注意：與歸結(jié)反演系統(tǒng)相對偶

目標表達式的形式是文字的析取，各文字的變量符號都不相同。這是因為 (x)[X1(x)∨X2(x)]≡ [(x)X1(x)∨(y)X2(y)]86例： 事實 P(A,B)∨[Q(x,A)∧R(B,y)] 規(guī)則 P(x,y)S(x)∨X(y) 目標 Q(C,A)∨R(z,B)∨S(A)∨X(B)--x,y均為全稱變量--z為存在變量87S(A) X(B)S(A) X(B) Q(C,A) R(z,B) {C/x}{B/z,B/y}P(x,y) Q(x,A) R(B,y) {A/x,B/y}P(A,B) Q(x,A)∧R(B,y)

P(A,B)∨[Q(x,A)∧R(B,y)]88一致解圖：具有一致的匹配弧置換的解圖?；卮鹫Z句：對該解圖對應的子句應用置換的合一復合而得到的例。置換的一致性和置換的合一復合的定義：設(shè)有一個置換集 U={u1,u2,…,un}, 其中 ui={ti1/vi1,…,tim(i)/vim(i)}，令 U1=(v11,…,v1m(1),…,vn1,…,vnm(n)) U2=(t11,…,t1m(1),…,tn1,…,tnm(n))如果U1和U2是可合一的，則稱U是一致的，而U的合一復合u=mgu(U1,U2)。89例： u1={x/y,x/z},u2={A/z} U1=(y,z,z),U2=(x,x,A) (y,z,z),(