演示文稿人工智能第三章

（優(yōu)選）人工智能第三章當(dāng)前1頁，總共79頁。謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)Skolem標(biāo)準(zhǔn)形 前束范式中消去所有的量詞。Skolem函數(shù)如果某個存在量詞是在其他任意量詞的轄域內(nèi)，就存在某種依賴關(guān)系，可以用一個函數(shù)描述這種依賴關(guān)系，叫做Skolem函數(shù)。當(dāng)前2頁，總共79頁。謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)量詞消去原則：存在量詞。將該量詞約束的變量用任意常量（a，b等）或任意變量的函數(shù)（f(x)，g(y)等）代替。左邊有任意量詞的存在量詞，消去時該變量改寫成為任意量詞的函數(shù)；如沒有，改寫成為常量。任意量詞。簡單地省略掉該量詞。當(dāng)前3頁，總共79頁。謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)例:將下式化為Skolem標(biāo)準(zhǔn)形： ～((x)(y)P(a,x,y)→(x)(～(y)Q(y,b)→R(x)))解：第一步，消去→，得： ～((～(x)(y)P(a,x,y))∨(x)(～～(y)Q(y,b)∨R(x)))第二步，～深入到量詞內(nèi)部，得：(x)(y)P(a,x,y)∧～(x)((y)Q(y,b)∨R(x))＝(x)(y)P(a,x,y)∧(x)((y)～Q(y,b)∧～R(x))第三步，任意量詞左移，得：

(x)(y)P(a,x,y)∧(y)(～Q(y,b)∧～R(x))當(dāng)前4頁，總共79頁。謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)

第四步，變量易名，存在量詞左移，直至所有的量詞移到前面，得：

(x)(y)P(a,x,y)∧(y)(～Q(y,b)∧～R(x))

＝(x)(y)P(a,x,y)∧(z)(～Q(z,b)∧～R(x))

＝(x)(y)(z)(P(a,x,y)∧～Q(z,b)∧～R(x))由此得到前述范式當(dāng)前5頁，總共79頁。謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)

第五步，消去存在量詞，略去任意量詞 消去(y)，因為它左邊只有(x)，所以使用x的函數(shù)f(x)代替，這樣得到：

(x)(z)(P(a,x,f(x))∧～Q(z,b)∧～R(x))

消去(z)，同理使用g(x)代替，這樣得到：

(x)(P(a,x,f(x))∧～Q(g(x),b)∧～R(x))

略去任意量詞，原式的Skolem標(biāo)準(zhǔn)形為：

P(a,x,f(x))∧～Q(g(x),b)∧～R(x)

當(dāng)前6頁，總共79頁。謂詞歸結(jié)子句形(Skolem標(biāo)準(zhǔn)形)Skolem定理： 謂詞邏輯的任意公式都可以化為與之等價的前束范式，但其前束范式不唯一。注意：謂詞公式G的Skolem標(biāo)準(zhǔn)形同G并不等值。

當(dāng)前7頁，總共79頁。謂詞歸結(jié)子句形子句與子句集文字：不含任何連接詞的謂詞公式。子句：一些文字的析?。ㄖ^詞的和）。空子句：不含任何文字的子句。記作NIL或□子句集：所有子句的集合。對于任何一個謂詞公式G，都可以通過Skolem標(biāo)準(zhǔn)形，建立起一個子句集與之對應(yīng)。當(dāng)前8頁，總共79頁。謂詞歸結(jié)子句形子句集S的求?。簩⒅^詞公式G轉(zhuǎn)換成前束范式；生成Skolem標(biāo)準(zhǔn)形；將各個子句提出，以“，”取代“Λ”，并表示為集合形式。當(dāng)前9頁，總共79頁。謂詞歸結(jié)子句形

定理3.1謂詞公式G是不可滿足的，當(dāng)且僅當(dāng)其子句集S是不可滿足的。G與S不等價，但在不可滿足的意義下是一致的。

注意：G真不一定S真，而S真必有G真。 即：S=>G當(dāng)前10頁，總共79頁。謂詞歸結(jié)子句形定理3.1的推廣對于形如G=G1ΛG2ΛG3Λ…ΛGn

的謂詞公式G的子句集可以分解成幾個部分單獨處理。有SG=S1US2US3U…USn

則SG

與S1US2US3U…USn在不可滿足的意義上是一致的。即SG

不可滿足<=>S1US2US3U…USn不可滿足?？梢詫σ粋€復(fù)雜的謂詞公式分而治之。當(dāng)前11頁，總共79頁。求取子句集例(1)例：對所有的x,y,z來說，如果y是x的父親，z又是y的父親，則z是x的祖父。又知每個人都有父親，試問對某個人來說誰是他的祖父？求：用一階邏輯表示這個問題，并建立子句集。解：這里我們首先引入謂詞：

P(x,y)表示y是x的父親

Q(x,y)表示y是x的祖父

ANS(x)表示問題的解答當(dāng)前12頁，總共79頁。求取子句集例(2)對于第一個條件，“如果y是x的父親，z又是y的父親，則z是x的祖父”，一階邏輯表達(dá)式如下：

A1：(x)(y)(z)(P(x,y)∧P(y,z)→Q(x,z)) SA1：～P(x,y)∨～P(y,z)∨Q(x,z)對于第二個條件：“每個人都有父親”，一階邏輯表達(dá)式：

A2：(x)(y)P(x,y) SA2：P(x,f(x))對于結(jié)論：某個人是他的祖父

B：(x)(y)Q(x,y)

否定后得到子句：～((x)(y)Q(x,y))∨ANS(y) S～B：～Q(x,y)∨ANS(y)則得到的相應(yīng)的子句集為：{SA1，SA2，S～B}當(dāng)前13頁，總共79頁。置換與合一一階謂詞邏輯得歸結(jié)比命題邏輯的歸結(jié)要復(fù)雜的多，其中一個原因就是謂詞邏輯公式中含有個體變量與函數(shù)。如P(x)∨Q(y)與~P(a)∨R(z)所以要考慮置換與合一。即對變量作適當(dāng)?shù)奶鎿Q。當(dāng)前14頁，總共79頁。置換置換：可以簡單的理解為是在一個謂詞公式中用置換項去置換變量。定義： 置換是形如{t1/x1,t2/x2,…,tn/xn}的有限集合。其中，x1,x2,…,xn是互不相同的變量，t1,t2,…,tn是不同于xi的項（常量、變量、函數(shù)）；ti/xi表示用ti置換xi，并且要求ti與xi不能相同，而且xi不能循環(huán)地出現(xiàn)在另一個ti中。例如：

{a/x，c/y，f(b)/z}是一個置換。

{g(y)/x，f(x)/y}不是一個置換。

當(dāng)前15頁，總共79頁。置換的合成設(shè)＝{t1/x1,t2/x2,…,tn/xn}， ＝{u1/y1,u2/y2,…,un/yn}，是兩個置換。 則與的合成也是一個置換，記作·。它是從集合

{t1·/x1,t2·/x2,…,tn·/xn,u1/y1,u2/y2,…,un/yn}

中刪去以下兩種元素：當(dāng)ti=xi時，刪去ti/xi(i=1,2,…,n);

當(dāng)yi{x1,x2,…,xn}時，刪去uj/yj

(j=1,2,…,m)

最后剩下的元素所構(gòu)成的集合。合成即是對ti先做置換然后再做置換當(dāng)前16頁，總共79頁。置換的合成例：設(shè)：＝{f(y)/x,z/y}，＝{a/x,b/y,y/z}，求與的合成。解：先求出集合

{f(b/y)/x,(y/z)/y,a/x,b/y,y/z}＝{f(b)/x,y/y,a/x,b/y,y/z}

其中，f(b)/x中的f(b)是置換作用于f(y)的結(jié)果；y/y中的y是置換作用于z的結(jié)果。在該集合中，y/y滿足定義中的條件i，需要刪除；a/x，b/y滿足定義中的條件ii，也需要刪除。最后得

·＝{f(b)/x，y/z}當(dāng)前17頁，總共79頁。合一合一可以簡單地理解為“尋找相對變量的置換，使兩個謂詞公式一致”。定義：設(shè)有公式集F＝{F1，F(xiàn)2，…，F(xiàn)n}，若存在一個置換，可使F1＝F2＝…=Fn，則稱是F的一個合一。同時稱F1，F(xiàn)2，...，F(xiàn)n是可合一的。

例： 設(shè)有公式集F＝{P(x,y,f(y)),P(a,g(x),z)}，則＝{a/x,g(a)/y,f(g(a))/z}是它的一個合一。注意：一般說來，一個公式集的合一不是唯一的。

當(dāng)前18頁，總共79頁。最一般合一（mgu）設(shè)σ是謂詞公式集F的一個合一，如果對F的任意一個合一都存在一個置換λ，使得θ=σ.λ，則稱σ是一個最一般合一。最一般合一求取方法令W={F1,F2}令k=0,W0=W,σ0=ε如果Wk已合一，停止，σk=mgu,否則找Dk若Dk中存在元素vk和tk，其中，vk不出現(xiàn)在tk中，轉(zhuǎn)下一步，否則，不可合一。令σk+1=σk.{tk/vk},Wk+1=Wk{tk/vk}=Wσk+1K=k+1轉(zhuǎn)第3步。當(dāng)前19頁，總共79頁。最一般合一（mgu）例：W={P(a,x,f(g(y))),P(z,f(a),f(u))},其中，F(xiàn)1＝P(a,x,f(g(y)))，F(xiàn)2＝P(z,f(a),f(u))求F1和F2的mgu解：由mgu算法(1)W={P(a,x,f(g(y))),P(z,f(a),f(u))}(2)W0=W,σ0=ε(3)W0未合一，從左到右找差異集，有D0={a,z}(4)取V0=z,t0＝a當(dāng)前20頁，總共79頁。最一般合一（mgu）(5)令σ1=σ0.{t0/v0}={a/z}W1=W0σ1={P(a,x,f(g(y))),P(a,f(a),f(u))}(3)’W1未合一，找差異集，有D1={x,f(a)}(4)’取v1=x,t1＝f(a)(5)’令σ2=σ1.{t1/v1}={a/z,f(a)/x}W2=W1σ2={P(a,f(a),f(g(y))),P(a,f(a),f(u))}(3)’’W2未合一，找差異集，有D2={g(y),u}(4)’’取v2=u,t2＝g(y)當(dāng)前21頁，總共79頁。最一般合一（mgu）(5)’’令σ3=σ2.{t2/v2}={a/z,f(a)/x,g(y)/u}W3=W2σ3={P(a,f(a),f(g(y))),P(a,f(a),f(g(y)))}(3)’’’W3已合一

σ3={a/z,f(a)/x,g(y)/u}便是F1和F2的mgu。算法的第(4)步，當(dāng)不存在vk或不存在tk或出現(xiàn)差異集為{x,f(x)},都會導(dǎo)致不可合一。此時，算法返回失敗。當(dāng)前22頁，總共79頁。最一般合一（mgu）

謂詞邏輯的歸結(jié)方法和命題邏輯基本相同，但在進(jìn)行歸結(jié)之前，應(yīng)采用最一般合一方法對待歸結(jié)的一對子句進(jìn)行置換。然后再判斷是否可以進(jìn)行歸結(jié)。當(dāng)前23頁，總共79頁。歸結(jié)原理歸結(jié)時的注意事項：謂詞的一致性，P()與Q()，不可以常量的一致性，P(a,…)與P(b,….)，不可以。變量與函數(shù)，P(a,x,….)與P(x,f(x),…)，不可以；不能同時消去兩個互補(bǔ)對，P∨Q與～P∨～Q得空，不可以先進(jìn)行內(nèi)部簡化再進(jìn)行置換與合并。

當(dāng)前24頁，總共79頁。歸結(jié)原理歸結(jié)的過程寫出謂詞關(guān)系公式→用反演法寫出謂詞表達(dá)式→SKOLEM標(biāo)準(zhǔn)形→求子句集S→對S中可歸結(jié)的子句做歸結(jié)→歸結(jié)式仍放入S中，反復(fù)歸結(jié)過程→得到空子句命題得證。當(dāng)前25頁，總共79頁。例題“快樂學(xué)生”問題例：假設(shè)任何通過計算機(jī)考試并獲獎的人都是快樂的，任何肯學(xué)習(xí)或幸運的人都可以通過所有的考試，張不肯學(xué)習(xí)但他是幸運的，任何幸運的人都能獲獎。求證：張是快樂的。

解：先將問題用謂詞表示如下：R1:任何通過計算機(jī)考試并獲獎的人都是快樂的(x)((Pass(x,computer)∧Win(x,prize))→Happy(x))R2:“任何肯學(xué)習(xí)或幸運的人都可以通過所有考試”

(x)(y)(Study(x)∨Lucky(x)→Pass(x,y))當(dāng)前26頁，總共79頁。例題“快樂學(xué)生”問題R3:“張不肯學(xué)習(xí)但他是幸運的” ～Study(zhang)∧Lucky(zhang)R4:“任何幸運的人都能獲獎”

(x)(Luck(x)→Win(x,prize))結(jié)論：“張是快樂的”的否定～Happy(zhang)當(dāng)前27頁，總共79頁。由R1及邏輯轉(zhuǎn)換公式:P∧W→H=～（P∧W）∨H，得

(1)～Pass(x,computer)∨～Win(x,prize)∨Happy(x)由R2：(2)～Study(y)∨Pass(y,z)(3)～Lucky(u)∨Pass(u,v)由R3：(4)～Study(zhang)(5)Lucky(zhang)由R4：(6)～Lucky(w)∨Win(w，prize)由結(jié)論：(7)～Happy(zhang) （結(jié)論的否定）(8)～Pass(w,computer)∨Happy(w)∨～Luck(w)(1)(6)，{w/x}(9)～Pass(zhang,computer)∨～Lucky(zhang)(8)(7)，{zhang/w}(10)

～Pass(zhang,computer) (9)(5)(11)

～Lucky(zhang)(10)(3)，{zhang/u,computer/v}(12)

?

(11)(5)

當(dāng)前28頁，總共79頁。第三章謂詞邏輯與歸結(jié)原理概述命題邏輯謂詞邏輯的歸結(jié)法歸結(jié)過程的控制策略Herbrand定理當(dāng)前29頁，總共79頁。第三章謂詞邏輯與歸結(jié)原理概述命題邏輯謂詞邏輯的歸結(jié)法歸結(jié)過程的控制策略Herbrand定理當(dāng)前30頁，總共79頁。歸結(jié)過程的控制策略要解決的問題：歸結(jié)方法的知識爆炸?？刂撇呗缘哪康臍w結(jié)點盡量少控制策略的原則給出控制策略，以使僅對選擇合適的子句間方可做歸結(jié)。避免多余的、不必要的歸結(jié)式出現(xiàn)?；蛘哒f，少做些歸結(jié)仍能導(dǎo)出空子句。當(dāng)前31頁，總共79頁?？刂撇呗缘姆椒?1)刪除策略歸類：設(shè)有兩個子句C和D，若有置換使得C

D成立，則稱子句C把子句D歸類。若對S使用歸結(jié)推理過程中，當(dāng)歸結(jié)式Cj是重言式和Cj被S中子句和子句集的歸結(jié)式Ci(i<j)所歸類時，便將Cj刪除。這樣的推理過程便稱作使用了刪除策略的歸結(jié)過程。當(dāng)前32頁，總共79頁?？刂撇呗缘姆椒?1)刪除策略如P(x)∨～P(x),P(x)∨Q(x)～P(x)P(x)歸類P(y)∨Q(z)σ={y/x}純文字刪除。如果某文字L在子句集中不存在可與之互補(bǔ)的文字～L，則稱該文字為純文字。如S={P∨Q∨R,～Q∨R,Q,～R}盡管使用刪除策略的歸結(jié)，少做了歸結(jié)但不影響產(chǎn)生空子句，就是說刪除策略的歸結(jié)推理是完備的。當(dāng)前33頁，總共79頁?？刂撇呗缘姆椒?2)支撐集策略支撐集：設(shè)有不可滿足子句集S的子集T，如果S-T是可滿足的，則T是支撐集。

采用支撐集策略時，從開始到得到空子句的整個歸結(jié)過程中，只選取不同時屬于S-T的子句，在其間進(jìn)行歸結(jié)。就是說，至少有一個子句來自于支撐集T或由T導(dǎo)出的歸結(jié)式。

當(dāng)前34頁，總共79頁?？刂撇呗缘姆椒?2)支撐集策略例如：A1ΛA2ΛA3Λ～B中的～B可以作為支撐集使用。要求每一次參加歸結(jié)的親本子句中，至少應(yīng)該有一個是由目標(biāo)公式的否定（～B）所得到的子句或者它們的后裔。支撐集策略的歸結(jié)是完備的。同樣，所有可歸結(jié)的謂詞公式都可以用采用支撐集策略達(dá)到加快歸結(jié)速度的目的。問題是如何尋找合適的支撐集。一個最容易找到的支撐集是目標(biāo)子句的非，即S～B。

當(dāng)前35頁，總共79頁。ST可滿足支撐集示意圖當(dāng)前36頁，總共79頁。控制策略的方法(2)支撐集策略例如：S(1)～I(xiàn)(X)∨R(X)目標(biāo)公式的否定得到的子句(2)I(a)(3)～R(Y)V～L(Y)(4)L(a)S1：(5)R(a)(1)與(2)歸結(jié)(6)～I(xiàn)(x)V～L(x)(1)與(3)歸結(jié)(7)～L(a)(2)與(6)歸結(jié)(8)NIL(4)與(7)歸結(jié)當(dāng)前37頁，總共79頁?？刂撇呗缘姆椒?3)語義歸結(jié)策略語義歸結(jié)策略是將子句S按照一定的語義分成兩部分，約定每部分內(nèi)的子句間不允許作歸結(jié)。同時還引入了文字次序，約定歸結(jié)時其中的一個子句的被歸結(jié)文字只能是該子句中“最大”的文字。語義歸結(jié)策略的歸結(jié)是完備的。當(dāng)前38頁，總共79頁?？刂撇呗缘姆椒?4)線性歸結(jié)線性歸結(jié)策略首先從子句集中選取一個稱作頂子句的子句C0開始作歸結(jié)。歸結(jié)過程中所得到的歸結(jié)式Ci立即同另一子句Bi進(jìn)行歸結(jié)得歸結(jié)式Ci+1。而Bi屬于S或是已出現(xiàn)的歸結(jié)式Cj(j<i)。即，如下圖所示歸結(jié)得到的新子句立即參加歸結(jié)。線性歸結(jié)是完備的。當(dāng)前39頁，總共79頁。C0C1C2C3C4C5空線性歸結(jié)策略示意圖當(dāng)前40頁，總共79頁?？刂撇呗缘姆椒?5)單元歸結(jié)策略單元歸結(jié)策略要求在歸結(jié)過程中，每次歸結(jié)都有一個子句是單元子句（只含一個文字的子句）或單元因子。顯而易見，此種方法可以簡單地削去另一個非單子句中的一個因子，使其長度減少，構(gòu)成簡單化，歸結(jié)效率較高。初始子句集中沒有單元子句時，單元歸結(jié)策略無效。所以說“反之不成立”，即此問題不能采用單元歸結(jié)策略。當(dāng)前41頁，總共79頁?？刂撇呗缘姆椒?6)輸入歸結(jié)策略與單元歸結(jié)策略相似，輸入歸結(jié)策略要求在歸結(jié)過程中，每一次歸結(jié)的兩個子句中必須有一個是S的原始子句。這樣可以避免歸結(jié)出的不必要的新子句加入歸結(jié)，造成惡性循環(huán)。可以減少不必要的歸結(jié)次數(shù)。如同單元歸結(jié)策略，不是所有的可歸結(jié)謂詞公式的最后結(jié)論都是可以從原始子句集中的得到的。當(dāng)前42頁，總共79頁。第三章謂詞邏輯與歸結(jié)原理概述命題邏輯謂詞邏輯的歸結(jié)法歸結(jié)過程的控制策略Herbrand定理當(dāng)前43頁，總共79頁。第三章謂詞邏輯與歸結(jié)原理概述命題邏輯謂詞邏輯的歸結(jié)法歸結(jié)過程的控制策略Herbrand定理當(dāng)前44頁，總共79頁。Herbrand定理問題： 一階邏輯公式的永真性（永假性）的判定是否能在有限步內(nèi)完成？當(dāng)前45頁，總共79頁。Herbrand定理1936年圖靈(Turing)和邱吉(Church)互相獨立地證明了：

“沒有一般的方法使得在有限步內(nèi)判定一階邏輯的公式是否是永真（或永假）。但是如果公式本身是永真（或永假）的，那么就能在有限步內(nèi)判定它是永真（或永假）。對于非永真（或永假）的公式就不一定能在有限步內(nèi)得到結(jié)論。判定的過程將可能是不停止的?！?/p>

當(dāng)前46頁，總共79頁。Herbrand定理Herbrand的思想定義： 公式G永真：對于G的所有解釋，G都為真。思想：

尋找一個已給的公式是真的解釋。然而，如果所給定的公式的確是永假的，就沒有這樣的解釋存在，并且算法在有限步內(nèi)停止。當(dāng)前47頁，總共79頁。Herbrand定理H域H解釋語義樹結(jié)論：Herbrand定理當(dāng)前48頁，總共79頁。Herbrand定理H域H解釋語義樹結(jié)論：Herbrand定理當(dāng)前49頁，總共79頁。Herbrand定理（H域）基本方法：因為量詞是任意的，所討論的個體變量域D是任意的，所以解釋的個數(shù)是無限、不可數(shù)的。簡化討論域。建立一個比較簡單、特殊的域，使得只要在這個論域上，該公式是不可滿足的。此域稱為H域。

當(dāng)前50頁，總共79頁。D域H域H域與D域關(guān)系示意圖當(dāng)前51頁，總共79頁。H域例題設(shè)子句集S={P(x),Q(y,f(z,b)),R(a)}，求H域解：H0

＝{a,b}為子句集中出現(xiàn)的常量H1

＝{a,b,f(a,b),f(a,a),f(b,a),f(b,b)}H2

＝{a,b,f(a,b),f(a,a),f(b,a),f(b,b)，f(a,f(a,b)),f(a,f(a,a)),f(a,f(b,a)),f(a,f(b,b)),f(b,f(a,b)),f(b,f(a,a)),f(b,f(b,a)),f(b,f(b,b)),f(f(a,b),f(a,b)),f(f(a,b),f(a,a)),f(f(a,b),f(b,a)),f(f(a,b),f(b,b)),f(f(a,a),f(a,b)),f(f(a,a),f(a,a)),f(f(a,a),f(b,a)),f(f(a,a),f(b,b)),f(f(b,a),f(a,b)),f(f(b,a),f(a,a)),f(f(b,a),f(b,a)),f(f(b,a),f(b,b)),f(f(b,b),f(a,b)),f(f(b,b),f(a,a)),f(f(b,b),f(b,a)),f(f(b,b),f(b,b))}

……… H∞=H1∪H2∪H3………當(dāng)前52頁，總共79頁。Herbrand定理（H域）幾個基本概念f（tn）：f為子句集S中的所有函數(shù)變量。t1,t2,…tn為S的H域的元素。通過它們來討論永真性。原子集A：謂詞套上H域的元素組成的集合。如

A={所有形如P(t1,t2,…tn)的元素}

即把H中的東西填到S的謂詞里去。S中的謂詞是有限的，H是可數(shù)的，因此，A也是可數(shù)的。當(dāng)前53頁，總共79頁。原子集例題上例題的原子集為：A={

P(a),Q(a,a),R(a),P(b),Q(b,a), Q(b,b),Q(a,b),R(b),P(f(a,b)),Q(f(a,b),f(a,b)),R(f(a,b),P(f(a,a)),P(f(b,a)),P(f(b,b)),……)

一旦原子集內(nèi)真值確定好（規(guī)定好），則S在H上的真值可確定。成為可數(shù)問題。當(dāng)前54頁，總共79頁。Herbrand定理H域H解釋語義樹結(jié)論：Herbrand定理當(dāng)前55頁，總共79頁。Herbrand定理H域H解釋語義樹結(jié)論：Herbrand定理當(dāng)前56頁，總共79頁。Herbrand定理（H解釋）解釋I：謂詞公式G在論域D上任何一組真值的指定稱為一個解釋。H解釋：子句集S在的H域上的解釋稱為H解釋。問題：對于所有的解釋，全是假才可判定。因為所有解釋代表了所有的情況，如可窮舉，問題便可解決。當(dāng)前57頁，總共79頁。Herbrand定理（H解釋）如下三個定理保證了歸結(jié)法的正確性：定理1：

設(shè)I是S的論域D上的解釋，存在對應(yīng)于I的H解釋I*，使得若有S|I=T，必有S|I*=T。定理2： 子句集S是不可滿足的，當(dāng)且僅當(dāng)所有的S的H解釋下為假。定理3： 子句集S是不可滿足的，當(dāng)且僅當(dāng)對每一個解釋I下，至少有S的某個子句的某個基例為假。當(dāng)前58頁，總共79頁。Herbrand定理（H解釋）基例S中某子句中所有變元符號均以S的H域中的元素代入時，所得的基子句C’稱為C的一個基例。若一個子句為假，則此解釋為假。一般來說，D是無窮不可列的，因此，子句集S也是無窮不可列的。但S確定后H是無窮可列的。不過在H上證明S的不可滿足性仍然是不可能的。解決問題的方法：語義樹當(dāng)前59頁，總共79頁。Herbrand定理H域H解釋語義樹結(jié)論：Herbrand定理當(dāng)前60頁，總共79頁。Herbrand定理H域H解釋語義樹結(jié)論：Herbrand定理當(dāng)前61頁，總共79頁。Herbrand定理（語義樹）構(gòu)成方法原子集中所有元素逐層添加的一棵二叉樹。將元素的是與非分別標(biāo)記在兩側(cè)的分枝上（可不完全畫完）。特點一般情況H是無限可數(shù)集，S的語義樹是無限樹。當(dāng)前62頁，總共79頁。N0P(a)N12Q(a)P(f(a))N24N31N38無限語義樹N11~P(a)~Q(a)Q(a)~Q(a)~P(f(a))N21S＝{～P(x)∨Q(x)，P(f(y))，～Q(f(y))}

當(dāng)前63頁，總共79頁。Herbrand定理（語義樹）意義SHA語義樹可以理解語義樹為H域的圖形解釋。目的：把每個解釋都攤開。語義樹中包含原子集的全部元素。因此，語義樹是完全的。每一個直到葉子節(jié)點的分支對應(yīng)S的一個解釋?？梢酝ㄟ^對語義樹每一個分支來計算S的真值。如果每個基例都為假，則可認(rèn)為是不可滿足的。當(dāng)前64頁，總共79頁。Herbrand定理（語義樹）幾個概念失敗結(jié)點： 當(dāng)（由上）延伸到點N時，I(N)已表明了S的某子句的某基例為假。但N以前尚不能判斷這個事實。就稱N為失敗結(jié)點。

封閉語義樹： 如果S的完全語義樹的每個分枝上都有一個失敗結(jié)點，就稱它是一棵封閉語義樹。當(dāng)前65頁，總共79頁。N0P(a)N1,2Q(a)P(f(a))N2,4N3,1N3,8N1,1N4,2N4,1N2,1N3,2N2,2N3,6N4,9N4,10N4,13N4,14封閉語義樹Q(f(a))S＝{～P(x)∨Q(x)，P(f(y))，～Q(f(y))}

當(dāng)前66頁，總共79頁。Herbrand定理H域H解釋語義樹結(jié)論：Herbrand定理當(dāng)前67頁，總共79頁。Herbrand定理H域H解釋語義樹結(jié)論：Herbrand定理當(dāng)前68頁，總共79頁。Herbrand定理（結(jié)論）Herbrand定理：子句集S是不可滿足的，當(dāng)且僅當(dāng)對應(yīng)于