三章演繹推理

1、第三章演繹推理自動定理證明是人工智能一個重要的研究領(lǐng)域，是早期取得較大成果的研究課題之一，在發(fā)展人工智能方法上起過重大作用。1956，美國，Newell,Simon,Shaw編制邏輯理論機(jī)：TheLogicTheoryMachine簡稱LT.證明了數(shù)學(xué)原理(羅素)第二章中38個定理，改進(jìn)后證明了全部52個定理。是對人的思維活動進(jìn)行研究的重大成果，是人工智能研究的真正開端。在此之后，發(fā)展了一些機(jī)械化推理算法，很成功地用到人工智能系統(tǒng)中。第一節(jié)魯濱遜歸結(jié)原理一、命題邏輯中歸結(jié)推理1歸結(jié)：消去子句中互補(bǔ)對的過程：子句：任何文字的析取式C稱為子句，C=PQ7R=P,Q,7R如:C仁LVC1'=

2、L,C1'C2=7LVC2'=7L,C2'可以證明C12=C1'VC2'=C1',C2'是C1,C2的邏輯結(jié)論：即:C1C2:C12證明：6=LVC1'=77C1'VL=7C1'LC2=7LVC2'=LC2'所以7C1'>C2'=77C1'VC2'=C1'VC2'實(shí)際上是P>Q,Q>吐>R的應(yīng)用即前提成立=結(jié)論成立，也即結(jié)論不成立=前提不成立S子句集：其中有C1,C2歸結(jié)式S'子句集：C12代替C1,C2貝U:S'

3、;不可滿足=S不可滿足2歸結(jié)推理步驟要證A=B成立(或證AB重言、永真),只要證A7B不可滿足(永假) 化A7B為合取范式C1C2Cm 子句集S=C1,C2,Cm 歸結(jié)規(guī)則用于S,歸結(jié)式入S中重復(fù)，直到S中出現(xiàn)空子句。證明：SVR是PQ,P>R,QS的邏輯結(jié)論。(PQ)(P>R)(QS)7(SR)=(PQ)(7PR)(7QS)7S7R所以S=PQ,7PR,7QS,7S,7R命題邏輯中不可滿足的子句集S,使用歸結(jié)原理，總能在有限步內(nèi)得到一個空子句=歸結(jié)原理是完備的。(1)PQ(2) 7PR(3) 7QS(4) 7S(5) 7RQR(1)(2)歸結(jié)(7)7Q(4)歸結(jié)(8)Q(6)歸結(jié)

4、(9)F(7)(8)歸結(jié)二、謂詞邏輯中的歸結(jié)原理謂詞和子句中含有個體變元，同一謂詞含有不同的個體變元。所以尋找互補(bǔ)對更困難。例：C1=P(y)Q(y)C2=7P(f(a)R(a)1.置換定義：形如t1/a1,t2/a2,tn/an的有限集合,表示ti代換ai，其中ti是項(xiàng)，變量，常量，函數(shù)。ai是變量，且ti不同于ai。置換的目的是使得S中有相同互補(bǔ)文字的子句中謂詞各對應(yīng)項(xiàng)變得一致，以便于歸結(jié)。0,表示置換。F0=G，貝UF0是F的邏輯推論。例如，F(xiàn)=P(x,f(x),y),P(a,z,g(z)做置換：1=a/x之后得：G1=F:1=P(a,f(a),y),P(a,z,g(z)：2=f(a)/

5、zG2=G1-2=P(a,f(a),y),P(a,f(a),g(f(a)：3=g(f(a)/yG3=G2：3=P(a,f(a),g(f(a),P(a,f(a),g(f(a)0=：1一12:3=a/x,f(a)/z,g(f(a)/y是一個置換.2合一定義：設(shè)有公式集F=F1,F2,Fn,若存在一個置換0,可使F10=F20=-=Fn0,則稱0為F的合一置換。稱F是可合一的。如上面“置換”一節(jié)中的例子。很明顯，很多F是不可合一的，而且一個公式集合的合一置換不唯一(如上例中，2=g(a)/y。定義：如果是公式集F的一個合一置換，且對F的任何一個合一0i，都存在一個置換i，使得0ii，則稱：.為F的最

6、一般合一.(MostGeneralUnifier簡記為MGU)最一般合一是最簡單的合一置換。求F的最一般合一方法：從左到右比較F中公式的對應(yīng)項(xiàng)，若不同則作置換，直到對應(yīng)項(xiàng)完全相同為止。3斯柯林范式：不含存在量詞和母式為合取范式的前束范式為斯柯林范式(x)(-y)(z)P(x,y,z)化為:(-y)P(a,y,f(y)(一x)(y)(z)Q(x,y,z)化為：(一x)Q(x,f(x),g(x)(x)(_y)(-z)(u)R(x,y,z.u)化為：(-y)(-z)R(a,y,z,f(y,z)4歸結(jié)推理過程例：C1=P(x)Q(x)C2=7P(a)R(y)令0=a/xC1'=C10=P(a)

7、Q(a)C2'=7P(a)R(y)=C12=Q(a)R(y)是C1,C2的邏輯推論定義：設(shè)C1和C2是兩個子句，L1,L2分別是C1和C2中的文字，如果0是L1與7L2的最一般合一，那么C12=(C10-L10)C20-C20為C1,C2的雙歸結(jié)式。如上例：L1=P(x),L2=7P(a)在一階謂詞中，對于不可滿足的子句集S,定可以在有限步內(nèi)推出空子句。所以謂詞邏輯中的歸結(jié)原理也是完備的。并非所有符號相同但變元不同的謂詞公式都可合一，如C1=P(x)Q(x)二C仁P(z)Q(z)C2=7P(f(x)R(y)所以要易名例：F1=(一x)(P(x)(Q(x)R(x)F2=(x)(P(x)S

8、(x)G=(x)(S(x)R(x)證明G是F1F2的邏輯推論證明:F1F27G=(一x)(7P(x)(Q(x)(R(x)(x)(P(x)S(x)(一x)(7S(x)7R(x)(7P(x)Q(x)(7P(x)R(x)P(a)S(a)(7S(x)7R(x)S=7P(x)Q(x),7P(y)R(y),P(a),S(a),7S(z)7R(z)歸結(jié)樹如下：7P(x)Q(x)7P(y)R(y)P(a)S(a)7S(z)7R(z)IIa/yR(a)IIa/z7R(a)IIF所以G是F1,F2的邏輯推論。例2:證明G是F1,F2的邏輯推論，其中：F1=(-x)(P(x)(-y)(Q(y)>7L(x,y)

9、F2=(x)(P(x)(y)(R(y)>L(x,y)G=(-x)(R(x)；7Q(x)解：對F1:(一x)(7P(x)(一y)(7Q(y)7L(x,y)S1=7P(x)7Q(y)7L(x,y)對F2:(P(a)(一y)(7R(y)L(a,y)S2=P(a),7R(z)L(a,z)對7G:(x)(77R(x)77Q(x)S3=R(b),Q(b)7P(x)7Q(y)7L(x,y)P(a)7R(z)L(a,z)R(b)Q(b)IIa/xIIb/z7Q(y)7L(a,y)L(a,b)IIb/y7Q(b)IIF5歸結(jié)策略用歸結(jié)推理方法可以證明S的子句不可滿足性由于該過程不斷產(chǎn)生新子句，因此，子句會

10、越來越多，同樣會出現(xiàn)組合爆炸問題。并且會產(chǎn)生大量的無用子句。因此在歸結(jié)中選擇哪兩個子句（含有互補(bǔ)對）進(jìn)行歸結(jié)，是一個控制策略問題。如果用樹來表示推理過程，就容易理解控制策略。演繹樹（倒長的樹）例如證S=7AB,A,D,7D7B不可滿足。7ABAD7D7BIIB7BIIF1）寬度優(yōu)先策略門第一級歸結(jié)：生成可能生成的全部歸結(jié)式S1,ST=S1S0第二級歸結(jié)：生成可能生成的全部歸結(jié)式S2,S2'=S2S1'（這時已進(jìn)行歸結(jié)的子句對不再歸結(jié)）直到生成空子句該方法效率低，但它是完備的。即只要子句集不可滿足，則一定能在有限步內(nèi)歸結(jié)得到空子句。例如證S=7AB,A,D,7D7B不可滿足。7A

11、VBAD7DV7B2）支持集優(yōu)先策略每次歸結(jié)時，要?dú)w結(jié)的兩個子句（親本子句）至少有一個是與目標(biāo)公式的否定式有關(guān)的子句（目標(biāo)公式的否定式化成的子句本身或它的有關(guān)后商）該策略完備？且效率高（相當(dāng)于在寬度優(yōu)是策略中有了啟發(fā)式信息）例如證DB是7AB，A,D的邏輯推論3）單元子句優(yōu)先策略每次歸結(jié)時，優(yōu)先選擇單文字子句作歸結(jié)（至少一個是原文字子句）。這樣得出的歸結(jié)式簡單，可能會提高效率。很顯然，這種歸結(jié)策略不完備。4）刪除策略刪除在歸結(jié)時產(chǎn)生的無用子句，從而減少了中子句數(shù)量?？梢詣h除下面子句：a. 永真式：P7P,Q7Qb. 重復(fù)出現(xiàn)的子句被歸類的子句：子句C把D歸類，當(dāng)且僅當(dāng)存在一個置換，使得CD,稱

12、D為被歸類子句。5）線性歸結(jié)首先選擇一個子句CO，與其它式作歸結(jié)產(chǎn)生C1，然后，對于新生成的Ci,i=1,2,n立刻被選中與其它子句Bi或Cj歸結(jié)，生成Ci+1。如果初始子句選擇得正確，線性歸結(jié)是完備的。類似深度優(yōu)先搜索方法。其中CO選擇是重要的，要選擇的是關(guān)鍵子句，即缺了CO剩余子句集可滿足，這是在支持集優(yōu)先策略上的改進(jìn)。6）組合策略：組合以上幾種方法。6應(yīng)用用于證明定理，如果x=A,W（x）真否？即x=A=W(x)取真?但x=?時,W(x)取真例1:事實(shí)：Johnlikeseverythingthatmarylikes.Marylikesreading.問：WhatdoesJohnlike?形式化：(-x)(L(Mary,x)rL(John