湘潭大學(xué)人工智能課件確定性推理part6

ArtificialIntelligence(AI)

人工智能第二章：知識表示與推理ArtificialIntelligence(AI)

人內(nèi)容提要第二章：知識表示與推理1.推理的基本概念2.搜索策略3.自然演繹推理4.消解演繹推理5.基于規(guī)則的演繹推理二、確定性推理內(nèi)容提要第二章：知識表示與推理1.推理的基本概念2.搜索策略消解演繹推理消解演繹推理子句集及其化簡魯濱遜消解原理消解反演推理的消解策略用消解反演求取問題的答案消解演繹推理消解演繹推理魯濱遜消解原理魯濱遜消解原理包括命題邏輯的消解謂詞邏輯的消解魯濱遜消解原理魯濱遜消解原理包括命題邏輯的消解命題邏輯的消解反演：在命題邏輯中，已知F，證明G為真的消解反演過程如下：①否定目標公式G，得﹁G;②把﹁G并入到公式集F中，得到{F，﹁G}；③把{F，﹁G}化為子句集S。④應(yīng)用消解原理對子句集S中的子句進行消解，并把每次得到的消解式并入S中。如此反復(fù)進行，若出現(xiàn)空子句，則停止消解，此時就證明了G為真。命題邏輯的消解命題邏輯的消解反演：在命題邏輯中，已知F，證明魯濱遜消解原理魯濱遜消解原理包括命題邏輯的消解謂詞邏輯的消解魯濱遜消解原理魯濱遜消解原理包括謂詞邏輯的消解在謂詞邏輯中，由于子句集中的謂詞一般都含有變元，因此不能象命題邏輯那樣直接消去互補文字。對于謂詞邏輯，需要先用一個最一般合一對變元進行置換，然后才能進行消解。謂詞邏輯的消解原理設(shè)C1和C2是兩個沒有公共變元的子句，L1和L2分別是C1和C2中的文字。如果σ是L1和﹁

L2存在最一般合一，則稱：C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})

為C1和C2的二元消解式，L1和L2為消解式上的文字。謂詞邏輯的消解在謂詞邏輯中，由于子句集中的謂詞一般都含有變元謂詞邏輯的消解例：設(shè)C1=P(a)∨R(x)，C2=﹁P(y)∨Q(b)，求C12解：取L1=P(a),L2=﹁P(y)，則L1和﹁L2的最一般合一是σ={a/y}。因此：C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})=({P(a),R(x)}-{P(a)})∪({﹁P(a),Q(b)}-{﹁P(a)})=({R(x)})∪({Q(b)})={R(x),Q(b)}=R(x)∨Q(b)謂詞邏輯的消解例：設(shè)C1=P(a)∨R(x)，C2=﹁P(y謂詞邏輯的消解例：設(shè)C1=P(x)∨Q(a)，C2=﹁P(b)∨R(x)，求C12解：由于C1和C2有相同的變元x，不符合定義的要求。為了進行消解，需要修改C2中變元的名字。令C2=﹁P(b)∨R(y)，此時L1=P(x),L2=﹁P(b)，L1和﹁L2的最一般合一是σ={b/x}。則有:

C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})=({P(b),Q(a)}-{P(b)})∪({﹁P(b),R(y)}-{﹁P(b)})=({Q(a)})∪({R(y)})={Q(a),R(y)}=Q(a)∨R(y)謂詞邏輯的消解例：設(shè)C1=P(x)∨Q(a)，C2=﹁P(b謂詞邏輯的消解例：設(shè)C1=P(a)∨﹁Q(x)∨R(x)

C2=﹁P(y)∨Q(b)求C12對C1和C2通過最一般合一（σ={b/x,a/y}）的作用，可以得到兩個互補對。注意：求消解式不能同時消去兩個互補對，這樣的結(jié)果不是二元消解式。如在σ={b/x,a/y}下，若同時消去兩個互補對，所得的R(b)不是C1和C2的二元消解式。謂詞邏輯的消解例：設(shè)C1=P(a)∨﹁Q(x)∨R(x)謂詞邏輯的消解例：設(shè)C1=P(a)∨﹁Q(x)∨R(x)

C2=﹁P(y)∨Q(b)求C12解1：取L1=P(a),L2=﹁P(y)，則σ={a/y}是L1與﹁L2的最一般合一。此時：

C12=﹁Q(x)∨R(x)∨Q(b)解2：取L1=﹁Q(x)，L2=Q(b)，則σ={b/x}是L1與﹁L2的最一般合一。此時：

C12=P(a)∨R(b)∨﹁P(y)謂詞邏輯的消解例：設(shè)C1=P(a)∨﹁Q(x)∨R(x)謂詞邏輯的消解例：設(shè)

C1=P(x)∨P(f(a))∨Q(x)，C2=﹁P(y)∨R(b)求C12解：對參加消解的某個子句，若其內(nèi)部有可合一的文字，則在進行消解之前應(yīng)先對這些文字進行合一。本例的C1中有可合一的文字P(x)與P(f(a))，若用它們的最一般合一σ={f(a)/x}進行代換，可得到：C1σ=P(f(a))∨Q(f(a))此時對C1σ與C2進行消解。選L1=P(f(a)),L2=﹁P(y)，L1和L2的最一般合一是σ={f(a)/y}，則可得到C1和C2的二元消解式為：

C12=R(b)∨Q(f(a))謂詞邏輯的消解例：設(shè)C1=P(x)∨P(f(a))∨Q(x謂詞邏輯的消解例：設(shè)C1=P(y)∨P(f(x))∨Q(g(x))

C2=﹁P(f(g(a)))∨Q(b)求C12解：對C1

，取最一般合一σ={f(x)/y}，得C1的因子

C1σ=P(f(x))∨Q(g(x))

對C1的因子和C2消解（σ={g(a)/x}），可得：

C12=Q(g(g(a)))∨Q(b)謂詞邏輯的消解例：設(shè)C1=P(y)∨P(f(x))∨Q(g謂詞邏輯的消解我們把C1σ稱為C1的因子。一般來說，若子句C中有兩個或兩個以上的文字具有最一般合一σ，則稱Cσ為子句C的因子。如果Cσ是一個單文字，則稱它為C的單元因子。應(yīng)用因子概念，可對謂詞邏輯中的消解原理給出如下定義：若C1和C2是無公共變元的子句，則子句C1和C2的消解式是下列二元消解式之一：①C1和C2的二元消解式;②C1的因子C1σ1和C2的二元消解式；③C1和C2的因子C2σ2的二元消解式；④C1的因子C1σ1和C2的因子C2σ的二元消解式。謂詞邏輯的消解我們把C1σ稱為C1的因子。一般來說，若子句C命題邏輯的消解反演：在命題邏輯中，已知F，證明G為真的消解反演過程如下：①否定目標公式G，得﹁G;②把﹁G并入到公式集F中，得到{F，﹁G}；③把{F，﹁G}化為子句集S。④應(yīng)用消解原理對子句集S中的子句進行消解，并把每次得到的消解式并入S中。如此反復(fù)進行，若出現(xiàn)空子句，則停止消解，此時就證明了G為真。謂詞邏輯的消解命題邏輯的消解反演：在命題邏輯中，已知F，證明G為真的消解反謂詞邏輯的消解謂詞邏輯的消解反演謂詞邏輯的消解反演過程與命題邏輯的消解反演過程相比，其步驟基本相同，但每步的處理對象不同。在步驟(3)化簡子句集時，謂詞邏輯需要把由謂詞構(gòu)成的公式集化為子句集。在步驟(4)按消解原理進行消解時，謂詞邏輯的消解原理需要考慮兩個親本子句的最一般合一。謂詞邏輯的消解謂詞邏輯的消解反演謂詞邏輯的消解例：已知F:(?x)((?y)(A(x,y)∧B(y))→(?y)(C(y)∧D(x,y)))G:﹁(?x)C(x)→(?x)(?y)(A(x,y)→﹁B(y))求證G是F的邏輯結(jié)論。證明：先把G否定，并放入F中，得到的{F,﹁G}：{(?x)((?y)(A(x,y)∧B(y))→(?y)(C(y)∧D(x,y))),

﹁(﹁(?x)C(x)→(?x)(?y)(A(x,y)→﹁B(y)))}再把{F,﹁G}化成子句集，得到謂詞邏輯的消解例：已知謂詞邏輯的消解

(1)﹁A(x,y)∨﹁B(y)∨C(f(x))(2)﹁A(u,v)∨﹁B(v)∨D(u,f(u))(3)﹁C(z)(4)A(m,n)(5)B(k)最后應(yīng)用謂詞邏輯的消解原理對上述子句集進行消解，其過程為：(6)﹁A(x,y)∨﹁B(y)

(7)﹁B(n)(8)NILF﹁G(1)和(3)消解，取σ={f(x)/z}(4)和(6)消解，取σ={m/x,n/y}(5)和(7)消解，取σ={n/k}謂詞邏輯的消解(1)﹁A(x,y)∨﹁B(y)∨C(謂詞邏輯的消解因此，G是F的邏輯結(jié)論。上述消解過程可用如下消解樹來表示﹁A(x,y)∨﹁B(y)∨C(f(x))﹁C(z)﹁A(x,y)∨﹁B(y)A(m,n)﹁B(n)B(k)NIL{f(x)/z}{m/x,n/y}{n/k}謂詞邏輯的消解因此，G是F的邏輯結(jié)論。﹁A(x,y)∨﹁謂詞邏輯的消解例：“快樂學(xué)生”問題假設(shè)：任何通過計算機考試并獲獎的人都是快樂的，任何肯學(xué)習(xí)或幸運的人都可以通過所有考試，張不肯學(xué)習(xí)但他是幸運的，任何幸運的人都能獲獎。求證：張是快樂的。解：先定義謂詞：Pass(x,y)：x可以通過y考試

Win(x,prize)：x能獲得獎勵

Study(x)：x肯學(xué)習(xí)

Happy(x)：x是快樂的

Lucky(x)：x是幸運的謂詞邏輯的消解例：“快樂學(xué)生”問題謂詞邏輯的消解再將問題用謂詞表示如下：“任何通過計算機考試并獎的人都是快樂的”(?x)(Pass(x,computer)∧Win(x,prize)→Happy(x))“任何肯學(xué)習(xí)或幸運的人都可以通過所有考試”

(?x)(?y)(Study(x)∨Lucky(x)→Pass(x,y))“張不肯學(xué)習(xí)但他是幸運的”

﹁Study(zhang)∧Lucky(zhang)“任何幸運的人都能獲獎”

(?x)(Lucky(x)→Win(x,prize))結(jié)論“張是快樂的”的否定

﹁Happy(zhang)謂詞邏輯的消解再將問題用謂詞表示如下：謂詞邏輯的消解將上述謂詞公式轉(zhuǎn)化為子句集如下：(1)﹁Pass(x,computer)∨﹁Win(x,prize)∨Happy(x)(2)﹁Study(y)∨Pass(y,z)(3)﹁Lucky(u)∨Pass(u,v)(4)﹁Study(zhang)(5)Lucky(zhang)(6)﹁Lucky(w)∨Win(w,prize)(7)﹁Happy(zhang)(結(jié)論的否定)按消解原理進行消解，消解樹如下：謂詞邏輯的消解將上述謂詞公式轉(zhuǎn)化為子句集如下：謂詞邏輯的消解﹁Pass(x,computer)∨﹁Win(x,prize)∨Happy(x)﹁Lucky(w)∨Win(w,prize)﹁Pass(w,Computer)∨Happy(w)∨﹁Lucky(w)﹁Happy(zhang)Lucky(zhang)﹁Pass(zhang,Computer)∨﹁Lucky(zhang)﹁Pass(zhang,Computer)﹁Lucky(u)∨Pass(u,v)﹁Lucky(zhang)Lucky(zhang)

NIL{w/x}{zhang/w}{zhang/u,computer/v}謂詞邏輯的消解﹁Pass(x,computer)∨﹁Win消解演繹推理消解演繹推理子句集及其化簡魯濱遜消解原理消解反演推理的消解策略用消解反演求取問題的答案消解演繹推理消解演繹推理消解反演推理的消解策略在消解演繹推理中，由于事先并不知道哪些子句對可進行消解，更不知道通過對哪些子句對的消解能盡快得到空子句，因此就需要對子句集中的所有子句逐對進行比較，直到得出空子句為止。這種盲目的全面進行消解的方法，不僅會產(chǎn)生許多無用的消解式，更嚴重的是會產(chǎn)生組核爆炸問題。因此，需要研究有效的消解策略來解決這些問題。常用的消解策略可分為兩大類：限制策略：通過限制參加消解的子句減少盲目性刪除策略：通過刪除某些無用的子句縮小消解范圍消解反演推理的消解策略在消解演繹推理中，由于事先并不知道哪些消解演繹推理消解演繹推理子句集及其化簡魯濱遜消解原理消解反演推理的消解策略用消解反演求取問題的答案消解演繹推理消解演繹推理用消解反演求取問題的答案消解原理出了可用于定理證明外，還可用來求取問題答案，其思想與定理證明相似。其一般步驟為：(1)把問題的已知條件用謂詞公式表示出來，并化為子句集；(2)把問題的目標的否定用謂詞公式表示出來，并化為子句集；(3)對目標否定子句集中的每個子句，構(gòu)造該子句的重言式（即把該目標否定子句和此目標否定子句的否定之間再進行析取所得到的子句），用這些重言式代替相應(yīng)的目標否定子句式，并把這些重言式加入到前提子句集中，得到一個新的子句集；(4)對這個新的子句集，應(yīng)用消解原理求出其證明樹，這時證明樹的根子句不為空，稱這個證明樹為修改的證明樹；(5)用修改證明樹的根子句作為回答語句，則答案就在此根子句中。用消解反演求取問題的答案消解原理出了可用于定理證明外，還可用用消解反演求取問題的答案例1：已知：“張和李是同班同學(xué)，如果x和y是同班同學(xué)，則x的教室也是y的教室，現(xiàn)在張在302教室上課?！眴枺骸艾F(xiàn)在李在哪個教室上課？”解：首先定義謂詞C(x,y)：x和y是同班同學(xué)At(x,u)：x在u教室上課。把已知前提用謂詞公式表示如下：C(zhang,li)(?x)(?y)(?u)(C(x,y)∧At(x,u)→At(y,u))At(zhang,302)用消解反演求取問題的答案例1：用消解反演求取問題的答案把目標的否定用謂詞公式表示如下：

﹁(?v)At(li,v)把上述公式化為子句集：

把目標的否定化成子句式，并用下面的重言式代替：

﹁At(li,v)∨At(li,v)把此重言式加入前提子句集中，得到一個新的子句集，對這個新的子句集，應(yīng)用消解原理求出其證明樹。C(zhang,li)﹁C(x,y)∨﹁At(x,u)∨At(y,u)At(zhang,302)用消解反演求取問題的答案把目標用消解反演求取問題的答案求解過程如下圖所示。該證明樹的根子句就是所求的答案，即“李明在302教室”。﹁At(li,v)∨At(li,v)﹁C(x,y)∨﹁At(x,u)∨At(y,u)At(li,v)∨﹁

C(x,li)∨﹁At(x,v)C(zhang,li)﹁At(zhang,v)∨At(li,v)At(zhang,302)At(li,302){li/y,v/u}{Zhang/x}{302/v}用消解反演求取問題的答案求解過程如下圖所示。該證明樹的根子句用消解反演求取問題的答案例2：已知：A,B,C三人中有人從不說真話，也有人從不說假話。某人向這三人分別提出同一個問題：誰是說謊者？A答：“B和C都是說謊者”；B答：“A和C都是說謊者”；C答：“A和B中至少有一個是說謊者”。問：求誰是老實人，誰是說謊者？解：首先定義謂詞T(x)：表示x說真話用消解反演求取問題的答案例2：用消解反演求取問題的答案把已知前提用謂詞公式表示如下：有人從不說真話：?T(C)∨?T(A)∨?T(B)有人從不說假話：T(C)∨T(A)∨T(B)根據(jù)“A答：B和C都是說謊者”，則若A說真話：T(A)→?T(B)∧?T(C)

若A說假話：

?T(A)→T(B)∨T(C)同理：根據(jù)“B答：A和C都是說謊者”，則T(B)→?T(A)∧?T(C)?T(B)→T(A)∨T(C)

根據(jù)“C答：A和B中至少有一個是說謊者”，則T(C)→?T(A)∨?T(B)?T(C)→T(A)∧T(B)用消解反演求取問題的答案把已知前提用謂詞公式表示如下：用消解反演求取問題的答案把上述公式化成子句集，得到前提子句集S：?T(A)∨?T(B)?T(A)∨?T(C)T(C)∨T(A)∨T(B)?T(B)∨?T(C)?T(C)∨?T(A)∨?T(B)T(A)∨T(C)T(B)∨T(C)先求誰是老實人，結(jié)論的否定為：?(?x)T(x)用消解反演求取問題的答案把上述公式化成子句集，得到前提子句集用消解反演求取問題的答案把目標的否定化成子句式，并用下面的重言式代替：

?T(x)∨T(x)把此重言式加入前提子句集S，得到一個新子句集，對這個新的子句集，應(yīng)用消解原理求出其證明樹。?T(A)∨?T(B)T(B)∨T(C)?T(A)∨T(C)T(A)∨T(C)T(C)?T(x)∨T(x)T(C){C/x}C是老實人用消解反演求取問題的答案把目標的否定化成子句式，并用下面的重用消解反演求取問題的答案下面證明A不是老實人，結(jié)論的否定為：?T(A)將結(jié)論的否定?

(?T(A))加入并入前提子句集S中，應(yīng)用消解原理對新的子句集進行消解：?T(A)∨?T(B)T(B)∨T(C)?T(A)∨T(C)?T(A)∨?T(C)?T(A)T(A)NIL得證。A不是是老實人同理可證B不是老實人用消解反演求取問題的答案下面證明A不是老實人，結(jié)論的否定為：消解演繹推理消解演繹推理的優(yōu)點：簡單，便于在計算機上實現(xiàn)。消解演繹推理的不足：必須把邏輯公式化成子句集。不便于閱讀與理解：?P(x)∨Q(x)沒有P(x)→Q(x)直觀。可能丟失控制信息，如下列邏輯公式：(?A∧?B)→C ?A→(B∨C)(?A∧?C)→B ?B→(A∨C)(?C∧?B)→A ?C→(B∨A)化成子句后都是:A∨B∨C消解演繹推理消解演繹推理的優(yōu)點：問題？問題？ArtificialIntelligence(AI)

人工智能第二章：知識表示與推理ArtificialIntelligence(AI)

人內(nèi)容提要第二章：知識表示與推理1.推理的基本概念2.搜索策略3.自然演繹推理4.消解演繹推理5.基于規(guī)則的演繹推理二、確定性推理內(nèi)容提要第二章：知識表示與推理1.推理的基本概念2.搜索策略消解演繹推理消解演繹推理子句集及其化簡魯濱遜消解原理消解反演推理的消解策略用消解反演求取問題的答案消解演繹推理消解演繹推理魯濱遜消解原理魯濱遜消解原理包括命題邏輯的消解謂詞邏輯的消解魯濱遜消解原理魯濱遜消解原理包括命題邏輯的消解命題邏輯的消解反演：在命題邏輯中，已知F，證明G為真的消解反演過程如下：①否定目標公式G，得﹁G;②把﹁G并入到公式集F中，得到{F，﹁G}；③把{F，﹁G}化為子句集S。④應(yīng)用消解原理對子句集S中的子句進行消解，并把每次得到的消解式并入S中。如此反復(fù)進行，若出現(xiàn)空子句，則停止消解，此時就證明了G為真。命題邏輯的消解命題邏輯的消解反演：在命題邏輯中，已知F，證明魯濱遜消解原理魯濱遜消解原理包括命題邏輯的消解謂詞邏輯的消解魯濱遜消解原理魯濱遜消解原理包括謂詞邏輯的消解在謂詞邏輯中，由于子句集中的謂詞一般都含有變元，因此不能象命題邏輯那樣直接消去互補文字。對于謂詞邏輯，需要先用一個最一般合一對變元進行置換，然后才能進行消解。謂詞邏輯的消解原理設(shè)C1和C2是兩個沒有公共變元的子句，L1和L2分別是C1和C2中的文字。如果σ是L1和﹁

L2存在最一般合一，則稱：C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})

為C1和C2的二元消解式，L1和L2為消解式上的文字。謂詞邏輯的消解在謂詞邏輯中，由于子句集中的謂詞一般都含有變元謂詞邏輯的消解例：設(shè)C1=P(a)∨R(x)，C2=﹁P(y)∨Q(b)，求C12解：取L1=P(a),L2=﹁P(y)，則L1和﹁L2的最一般合一是σ={a/y}。因此：C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})=({P(a),R(x)}-{P(a)})∪({﹁P(a),Q(b)}-{﹁P(a)})=({R(x)})∪({Q(b)})={R(x),Q(b)}=R(x)∨Q(b)謂詞邏輯的消解例：設(shè)C1=P(a)∨R(x)，C2=﹁P(y謂詞邏輯的消解例：設(shè)C1=P(x)∨Q(a)，C2=﹁P(b)∨R(x)，求C12解：由于C1和C2有相同的變元x，不符合定義的要求。為了進行消解，需要修改C2中變元的名字。令C2=﹁P(b)∨R(y)，此時L1=P(x),L2=﹁P(b)，L1和﹁L2的最一般合一是σ={b/x}。則有:

C12=({C1σ}-{L1σ})∪({C2σ}-{L2σ})=({P(b),Q(a)}-{P(b)})∪({﹁P(b),R(y)}-{﹁P(b)})=({Q(a)})∪({R(y)})={Q(a),R(y)}=Q(a)∨R(y)謂詞邏輯的消解例：設(shè)C1=P(x)∨Q(a)，C2=﹁P(b謂詞邏輯的消解例：設(shè)C1=P(a)∨﹁Q(x)∨R(x)

C2=﹁P(y)∨Q(b)求C12對C1和C2通過最一般合一（σ={b/x,a/y}）的作用，可以得到兩個互補對。注意：求消解式不能同時消去兩個互補對，這樣的結(jié)果不是二元消解式。如在σ={b/x,a/y}下，若同時消去兩個互補對，所得的R(b)不是C1和C2的二元消解式。謂詞邏輯的消解例：設(shè)C1=P(a)∨﹁Q(x)∨R(x)謂詞邏輯的消解例：設(shè)C1=P(a)∨﹁Q(x)∨R(x)

C2=﹁P(y)∨Q(b)求C12解1：取L1=P(a),L2=﹁P(y)，則σ={a/y}是L1與﹁L2的最一般合一。此時：

C12=﹁Q(x)∨R(x)∨Q(b)解2：取L1=﹁Q(x)，L2=Q(b)，則σ={b/x}是L1與﹁L2的最一般合一。此時：

C12=P(a)∨R(b)∨﹁P(y)謂詞邏輯的消解例：設(shè)C1=P(a)∨﹁Q(x)∨R(x)謂詞邏輯的消解例：設(shè)

C1=P(x)∨P(f(a))∨Q(x)，C2=﹁P(y)∨R(b)求C12解：對參加消解的某個子句，若其內(nèi)部有可合一的文字，則在進行消解之前應(yīng)先對這些文字進行合一。本例的C1中有可合一的文字P(x)與P(f(a))，若用它們的最一般合一σ={f(a)/x}進行代換，可得到：C1σ=P(f(a))∨Q(f(a))此時對C1σ與C2進行消解。選L1=P(f(a)),L2=﹁P(y)，L1和L2的最一般合一是σ={f(a)/y}，則可得到C1和C2的二元消解式為：

C12=R(b)∨Q(f(a))謂詞邏輯的消解例：設(shè)C1=P(x)∨P(f(a))∨Q(x謂詞邏輯的消解例：設(shè)C1=P(y)∨P(f(x))∨Q(g(x))

C2=﹁P(f(g(a)))∨Q(b)求C12解：對C1

，取最一般合一σ={f(x)/y}，得C1的因子

C1σ=P(f(x))∨Q(g(x))

對C1的因子和C2消解（σ={g(a)/x}），可得：

C12=Q(g(g(a)))∨Q(b)謂詞邏輯的消解例：設(shè)C1=P(y)∨P(f(x))∨Q(g謂詞邏輯的消解我們把C1σ稱為C1的因子。一般來說，若子句C中有兩個或兩個以上的文字具有最一般合一σ，則稱Cσ為子句C的因子。如果Cσ是一個單文字，則稱它為C的單元因子。應(yīng)用因子概念，可對謂詞邏輯中的消解原理給出如下定義：若C1和C2是無公共變元的子句，則子句C1和C2的消解式是下列二元消解式之一：①C1和C2的二元消解式;②C1的因子C1σ1和C2的二元消解式；③C1和C2的因子C2σ2的二元消解式；④C1的因子C1σ1和C2的因子C2σ的二元消解式。謂詞邏輯的消解我們把C1σ稱為C1的因子。一般來說，若子句C命題邏輯的消解反演：在命題邏輯中，已知F，證明G為真的消解反演過程如下：①否定目標公式G，得﹁G;②把﹁G并入到公式集F中，得到{F，﹁G}；③把{F，﹁G}化為子句集S。④應(yīng)用消解原理對子句集S中的子句進行消解，并把每次得到的消解式并入S中。如此反復(fù)進行，若出現(xiàn)空子句，則停止消解，此時就證明了G為真。謂詞邏輯的消解命題邏輯的消解反演：在命題邏輯中，已知F，證明G為真的消解反謂詞邏輯的消解謂詞邏輯的消解反演謂詞邏輯的消解反演過程與命題邏輯的消解反演過程相比，其步驟基本相同，但每步的處理對象不同。在步驟(3)化簡子句集時，謂詞邏輯需要把由謂詞構(gòu)成的公式集化為子句集。在步驟(4)按消解原理進行消解時，謂詞邏輯的消解原理需要考慮兩個親本子句的最一般合一。謂詞邏輯的消解謂詞邏輯的消解反演謂詞邏輯的消解例：已知F:(?x)((?y)(A(x,y)∧B(y))→(?y)(C(y)∧D(x,y)))G:﹁(?x)C(x)→(?x)(?y)(A(x,y)→﹁B(y))求證G是F的邏輯結(jié)論。證明：先把G否定，并放入F中，得到的{F,﹁G}：{(?x)((?y)(A(x,y)∧B(y))→(?y)(C(y)∧D(x,y))),

﹁(﹁(?x)C(x)→(?x)(?y)(A(x,y)→﹁B(y)))}再把{F,﹁G}化成子句集，得到謂詞邏輯的消解例：已知謂詞邏輯的消解

(1)﹁A(x,y)∨﹁B(y)∨C(f(x))(2)﹁A(u,v)∨﹁B(v)∨D(u,f(u))(3)﹁C(z)(4)A(m,n)(5)B(k)最后應(yīng)用謂詞邏輯的消解原理對上述子句集進行消解，其過程為：(6)﹁A(x,y)∨﹁B(y)

(7)﹁B(n)(8)NILF﹁G(1)和(3)消解，取σ={f(x)/z}(4)和(6)消解，取σ={m/x,n/y}(5)和(7)消解，取σ={n/k}謂詞邏輯的消解(1)﹁A(x,y)∨﹁B(y)∨C(謂詞邏輯的消解因此，G是F的邏輯結(jié)論。上述消解過程可用如下消解樹來表示﹁A(x,y)∨﹁B(y)∨C(f(x))﹁C(z)﹁A(x,y)∨﹁B(y)A(m,n)﹁B(n)B(k)NIL{f(x)/z}{m/x,n/y}{n/k}謂詞邏輯的消解因此，G是F的邏輯結(jié)論。﹁A(x,y)∨﹁謂詞邏輯的消解例：“快樂學(xué)生”問題假設(shè)：任何通過計算機考試并獲獎的人都是快樂的，任何肯學(xué)習(xí)或幸運的人都可以通過所有考試，張不肯學(xué)習(xí)但他是幸運的，任何幸運的人都能獲獎。求證：張是快樂的。解：先定義謂詞：Pass(x,y)：x可以通過y考試

Win(x,prize)：x能獲得獎勵

Study(x)：x肯學(xué)習(xí)

Happy(x)：x是快樂的

Lucky(x)：x是幸運的謂詞邏輯的消解例：“快樂學(xué)生”問題謂詞邏輯的消解再將問題用謂詞表示如下：“任何通過計算機考試并獎的人都是快樂的”(?x)(Pass(x,computer)∧Win(x,prize)→Happy(x))“任何肯學(xué)習(xí)或幸運的人都可以通過所有考試”

(?x)(?y)(Study(x)∨Lucky(x)→Pass(x,y))“張不肯學(xué)習(xí)但他是幸運的”

﹁Study(zhang)∧Lucky(zhang)“任何幸運的人都能獲獎”

(?x)(Lucky(x)→Win(x,prize))結(jié)論“張是快樂的”的否定

﹁Happy(zhang)謂詞邏輯的消解再將問題用謂詞表示如下：謂詞邏輯的消解將上述謂詞公式轉(zhuǎn)化為子句集如下：(1)﹁Pass(x,computer)∨﹁Win(x,prize)∨Happy(x)(2)﹁Study(y)∨Pass(y,z)(3)﹁Lucky(u)∨Pass(u,v)(4)﹁Study(zhang)(5)Lucky(zhang)(6)﹁Lucky(w)∨Win(w,prize)(7)﹁Happy(zhang)(結(jié)論的否定)按消解原理進行消解，消解樹如下：謂詞邏輯的消解將上述謂詞公式轉(zhuǎn)化為子句集如下：謂詞邏輯的消解﹁Pass(x,computer)∨﹁Win(x,prize)∨Happy(x)﹁Lucky(w)∨Win(w,prize)﹁Pass(w,Computer)∨Happy(w)∨﹁Lucky(w)﹁Happy(zhang)Lucky(zhang)﹁Pass(zhang,Computer)∨﹁Lucky(zhang)﹁Pass(zhang,Computer)﹁Lucky(u)∨Pass(u,v)﹁Lucky(zhang)Lucky(zhang)

NIL{w/x}{zhang/w}{zhang/u,computer/v}謂詞邏輯的消解﹁Pass(x,computer)∨﹁Win消解演繹推理消解演繹推理子句集及其化簡魯濱遜消解原理消解反演推理的消解策略用消解反演求取問題的答案消解演繹推理消解演繹推理消解反演推理的消解策略在消解演繹推理中，由于事先并不知道哪些子句對可進行消解，更不知道通過對哪些子句對的消解能盡快得到空子句，因此就需要對子句集中的所有子句逐對進行比較，直到得出空子句為止。這種盲目的全面進行消解的方法，不僅會產(chǎn)生許多無用的消解式，更嚴重的是會產(chǎn)生組核爆炸問題。因此，需要研究有效的消解策略來解決這些問題。常用的消解策略可分為兩大類：限制策略：通過限制參加消解的子句減少盲目性刪除策略：通過刪除某些無用的子句縮小消解范圍消解反演推理的消解策略在消解演繹推理中，由于事先并不知道哪些消解演繹推理消解演繹推理子句集及其化簡魯濱遜消解原理消解反演推理的消解策略用消解反演求取問題的答案消解演繹推理消解演繹推理用消解反演求取問題的答案消解原理出了可用于定理證明外，還可用來求取問題答案，其思想與定理證明相似。其一般步驟為：(1)把問題的已知條件用謂詞公式表示出來，并化為子句集；(2)把問題的目標的否定用謂詞公式表示出來，并化為子句集；(3)對目標否定子句集中的每個子句，構(gòu)造該子句的重言式（即把該目標否定子句和此目標否定子句的否定之間再進行析取所得到的子句），用這些重言式代替相應(yīng)的目標否定子句式，并把這些重言式加入到前提子句集中，得到一個新的子句集；(4)對這個新的子句集，應(yīng)用消解原理求出其證明樹，這時證明樹的根子句不為空，稱這個證明樹為修改的證明樹；(5)用修改證明樹的根子句作為回答語句，則答案就在此根子句中。用消解反演求取問題的答案消解原理出了可用于定理證明外，還可用用消解反演求取問題的答案例1：已知：“張和李是同班同學(xué)，如果x和y是同班同學(xué)，則x的教室也是y的教室，現(xiàn)在張在302教室上課?！眴枺骸艾F(xiàn)在李在哪個教室上課？”解：首先定義謂詞C(x,y)：x和y是同班同學(xué)At(x,u)：x在u教室上課。把已知前提用謂詞公式表示如下：C(zhang,li)(?x)(?y)(?u)(C(x,y)∧At(x,u)→At(y,u))At(zhang,302)用消解反演求取問題的答案例1：用消解反演求取問題的答案把目標的否定用謂詞公式表示如下：

﹁(?v)At(li,v)把上述公式化為子句集：

把目標的否定化成子句式，并用下面的重言式代替：

﹁At(li,v)∨At(li,v)把此重言式加入前提子句集中，得到一個新的子句集，對這個新的子句集，應(yīng)用消解原理求出其證明樹。C(zhang,li)﹁C(x,y)∨﹁At(x,u)∨At(y,u)At(zhang,302)用消解反演求取問題的答案把目標用消解反演求取問題的答案