【正文】 f(b,b)),……) ? 一旦原子集內(nèi)真值確定好（規(guī)定好），則 S在 H上的真值可確定。不可數(shù)問題轉(zhuǎn)化成為了可數(shù)問題。 S中的謂詞是有限的， H是可數(shù)的，因此， A也是可數(shù)的。 H解釋 ?解釋 I：謂詞公式 G在論域 D上任何一組真值的指定稱為一個(gè)解釋。 ?H解釋 ：子句集 S在 H域上的解釋稱為 H解釋。 ? I是 H域下的一個(gè)指派。凡對 A中各元素真假值的一個(gè)具體設(shè)定，都是 S的一個(gè) H解釋。 ? 由子句集 S建立 H域、原子集 A，希望定義于一般論域 D上使 S為真的任一解釋 I，可由依于 S的 H域上的某個(gè)解釋 I*來實(shí)現(xiàn)。這樣，便使任意論域 D上 S為真的問題，化成了僅有可數(shù)個(gè)元素的 H域上 S為真的問題了。從而子句集 S在 D上不可滿足問題化成了 H上的不可滿足的問題。 幾個(gè)術(shù)語的定義 ?沒有變量出現(xiàn)的原子、文字、子句和子句集，分別稱為 基原子、基文字、基子句和基子句集 。 ?基例 ：子句集 S中某子句 C中所有變元符號(hào)均以 S的H域中的元素代入時(shí)，所得的基子句 C?稱為 C的一個(gè)基例。 ?若一個(gè)解釋 I*使得某個(gè)基子句為假，則此解釋 I*為假。 關(guān)于基例 例 S={P(x),Q(f(y))∨R(y)} 有 H={a,f(a),f(f(a)),? } 對任一 b∈D, 子句 P(b),Q(f(b))∨R(b) 都叫 基子句 。 而 P(a),P(f(a))都稱作子句 C=P(x)的 基例 。 同樣 ， Q(f(a))∨R(a), Q(f(f(a)))∨R(f(a))都是子句 Q(f(y))∨R(y) 的 基例 。 例 ： S＝ {P(x)∨ Q(x), R(f(y))}，求其一個(gè) H解釋 I* 解 ： S的 H域?yàn)椋?{a, f(a), f(f(a)), …} S的原子集為： {P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)), 凡對 A中各元素真假值的一個(gè)具體設(shè)定都為 S的一個(gè) H解釋。 如： I1*＝ {P(a), Q(a), R(a), P(f(a)), Q(f(a)), R(f(a)), …} I2*＝ {～ P(a), ～ Q(a), ～ R(a), ～ P(f(a)), Q(f(a)), R(f(a)), …} I3*＝ {P(a), ～ Q(a), ～ R(a), P(f(a)), Q(f(a)), ～ R(f(a)), …} I1*， I2*， I3*中出現(xiàn)的 P(a)表示 P(a)的取值為 T，出現(xiàn)的～ P(a)表示 P(a)的取值為 F。顯然在 H域上，這樣的定義 I*下， S的真值就確定了。 如： S| I1*＝ T， S| I2*＝ F， S| I3*＝ F 這是因?yàn)? 子句集 S＝ {P(x)∨ Q(x), R(f(y))}的邏輯含義為： (?x)(?y)((P(x)∨ Q(x))∧ R(f(y)))， 論域 H為 {a, f(a), f(f(a)), …} 。 Herbrand定理 （ H解釋） ?關(guān)鍵問題 ：對于公式 G的所有的解釋，如果公式取值全為假，才可以判定 G是不可滿足的。因?yàn)樗薪忉尨砹怂械那闆r，如果這些解釋可以被窮舉，問題便可解決 。 ?對論域 D上的任一解釋 I,若有 S|I=T,如何求得一個(gè)相應(yīng)的 H解釋 I*,使得 S|I*=T成立。 ?由 I到 I*,實(shí)為 H域到 D域的映射 ,對 H中每個(gè)常量、每個(gè)函數(shù)依 I來規(guī)定 D中的一個(gè)確定的元素。 ?以下三個(gè)定理保證了歸結(jié)法的正確性。 定理 (1) 設(shè) I是 S的論域 D上的解釋 ,存在對應(yīng)于 I的 H解釋 I*,使得若有 S|I=T,必有 S|I*=T。 說明：由 I到 I*,實(shí)為 H域到 D域的映射 。 即：對 H中每個(gè)常量 、 每個(gè)函數(shù)依 I來規(guī)定 D中的一個(gè)確定的元素 。 定理 (2) 子句集 S是不可滿足的 ,當(dāng)且僅當(dāng)在所有的 S的 H解釋下為假 。 說明：這個(gè)定理將 S在一般論域 D上的不可滿足問題化成了可數(shù)集 H上的不可滿足問題 。 定理 (3) 子句集 S是不可滿足的，當(dāng)且僅當(dāng)對每個(gè)解釋 I下 ,至少有 S的某個(gè)子句的某個(gè)基例為假。 解釋：因?yàn)?S的邏輯含義是所包含的子句的合取 ,而且變量受全稱量詞作用。那么在某個(gè)解釋 I(均指 H解釋 )下為假 ,只需某個(gè)子句的某個(gè)基例為假 ,而S是不可滿足則要求在任一解釋下均為假。 語義樹與 Herbrand定理 ?從幾何上進(jìn)行討論，將子句集 S的所有可能解釋展示在一棵樹上，進(jìn)而觀察每個(gè)分枝對應(yīng)的 S的邏輯真值是真是假。 ?語義樹的構(gòu)成方法 ：原子集 A中所有元素逐層添加到一棵二叉樹，并將元素的 39。是 39。與 39。非 39。分別標(biāo)記在兩側(cè)的分枝上。 ?語義樹特點(diǎn) ：一般 H是無限可數(shù)集，因此， S的語義樹是無限樹。 語義樹的意義 ?語義樹可以理解為 H域的 圖形解釋 。 ?通過子句集 S → H 域 → 原子集 A → 語義樹，可見，討論的對象從無限、不可數(shù)論域 D轉(zhuǎn)換成了可數(shù)的、有序的語義樹。 ?建立語義樹的目的 ：把 S中的每個(gè)解釋都攤開。 S的完全語義樹的每個(gè)直到葉結(jié)點(diǎn) N的分枝都對應(yīng)于 S的一個(gè)解釋 I(N) 。討論 S的不可滿足性，可通過對語義樹的每個(gè)分枝計(jì)算 S的每一個(gè)解釋的真值而實(shí)現(xiàn)。如果每個(gè)基例都為假，則可認(rèn)為是不可滿足的。 ?有時(shí)并非需要無限地延伸某個(gè)分枝方能確定在相應(yīng)的解釋下 S取假值。如果某個(gè)分枝延伸到結(jié)點(diǎn) N時(shí)，I(N)已使 S的某一子句的某一基例為假，就無需再對N作延伸了。 例 1 設(shè)子句集 S的原子集 A={P,Q,R} 屬命題邏輯。這時(shí) S的原子集就是 S中出現(xiàn)的全體原子命題。 為了方便 ,常用 I(N34)={P,～ Q,～ R} 表示從根結(jié)點(diǎn)到結(jié)點(diǎn) N分枝上所標(biāo)記的所有文字的并集。 圖 S的語義樹是一棵 有限樹 。 語義樹中的幾個(gè)定義 ?完全語義樹： 如果對一棵語義樹的所有葉結(jié)點(diǎn) N來說 ,I(N)包含了 S的原子集 A={A1,A2,?} 中的所有元素 Ai或～ Ai（ i=1?n) ，就稱 S是 完全語義樹 。 ?失敗結(jié)點(diǎn)： 如果結(jié)點(diǎn) N的 I(N)使 S的某一子句的某一基例為假 ,而N的父輩結(jié)點(diǎn)不能判斷這個(gè)事實(shí) ,就說 N是 失敗結(jié)點(diǎn) 。 ?封閉樹： 如果 S的完全語義樹的每個(gè)分枝上都有一個(gè)失敗結(jié)點(diǎn) ,就說它是一棵 封閉樹 。 例 ： S＝ {～ P(x)∨ Q(x)， P(f(y))，～ Q(f(y))}，畫出其語義樹。 ?解 ：子句集 S的 H域?yàn)椋? H＝ {a， f(a)， f(f(a))， …} 原子集為： A＝ {P(a),Q(a),P(f(a)),Q(f(a)),…} 從 A出發(fā) 便可畫出 S的語義樹， 如圖 22所示。 前面圖 22所示的完全語義樹便具有每個(gè)分枝上都有失敗結(jié)點(diǎn)這樣的性質(zhì)，從而是一棵封閉的語義樹。如果從圖 22剪去所有失敗結(jié)點(diǎn)以下的分枝，便得相應(yīng)的封閉語義樹，見左圖 23。 ? 如 I(N22)={P(a),～ Q(a)},這個(gè) S的部分解釋已使 S中的子句～ P(x)∨Q(a) 的基例～ P(a)∨Q(a) 為假了 ,而 N11,N0不具有這個(gè)性質(zhì) 。 若將 I(N22)擴(kuò)充為 S的解釋 ,仍然會(huì)使 S為假 ,擴(kuò)充的部分對使 S為假已不起作用了 。 從圖上看無需對 N22再作延伸了 。 ? 再如， I(N41)={P(a),Q(a),P(f(a)),Q(f(a))},它使 S的子句～ Q(f(y))的基例～ Q(f(a))為假 ,而 N41的父輩不能使 S的某子句的某基例為假 ,從而 N41是失敗結(jié)點(diǎn)。同樣 ,為討論 S的不可滿足性無需對 N41做延伸了。 一個(gè)簡單的語義樹的倒塌過程 例 S={P,～ P∨ Q,～ P∨ ～ Q} A={P,Q},畫出語義樹 T 和相應(yīng)的封閉樹 T* (見圖 )。 歸結(jié)過程： (1)P (2)～ P ∨ Q (3)～ P ∨ ～ Q (4)～ P (2)(3)歸結(jié) (5)口 (1)(4)歸結(jié) ? 樹 T*上的 N11結(jié)點(diǎn) ,有子結(jié)點(diǎn) N21,N22對應(yīng)的 I(N21)={P,Q} 使子句 (3)為假。 I(N22)={P,～Q)使子句 (2)為假。從而 N21,N22都是失敗結(jié)點(diǎn)?？梢姡?N11有兩個(gè)分枝對應(yīng)的子結(jié)點(diǎn)都是失敗結(jié)點(diǎn) ,這時(shí)相應(yīng)的子句 (2)(3)必可做歸結(jié) （有歸結(jié)式 ～ P）。 ? 進(jìn)而將～ P并入 S得 S∪{ ～ P},這時(shí)的 I(N11)={P},已使 S∪{ ～ P}的子句～ P為假了。從而 N11是 S∪{ ～ P}的語義樹 (同 T)的失敗結(jié)點(diǎn)了 ,其封閉樹為 T(1)。 這就是說作一次歸結(jié) ,就使封閉語義樹倒塌兩個(gè)分枝 N11N21,N11N22,或說 N11N21,N11N22被剪枝了。 ? 對 T(1)的結(jié)點(diǎn) N0,有兩個(gè)分枝對應(yīng)的子結(jié)點(diǎn) N11,N12,都是 S∪{ ～ P}的失敗結(jié)點(diǎn) ,又I(N11)={P}使子句 (4)為假， I(N12)={～ P}使子句 (1)為假，這時(shí)的子句 (1)(4)又可做歸結(jié) ,有歸結(jié)式口。將口并入 S∪{ ～ P}得 S∪{ ～ P,口 }， N0已是失敗結(jié)點(diǎn) ,其封閉樹為T(2),是只剩下根結(jié)點(diǎn) N0的樹了。 歸結(jié)與語義樹“倒塌”過程 ? 上述例子說明，對子句集 S和相應(yīng)的語義樹 T， 當(dāng)將 S的任意兩子句的歸結(jié)式加入 S后，相應(yīng)的語義樹 T(1)較 T“ 倒塌”了兩個(gè)分枝；隨著不斷地歸結(jié)， T就不斷地“倒塌”； 當(dāng) S是不可滿足的， T將倒塌成只剩下根結(jié)點(diǎn)了 。 ?結(jié)論：歸結(jié)過程就是語義樹倒塌過程 。 若要證明有歸結(jié)過程使由 S可歸結(jié)出口，就可從 S的語義樹 T出發(fā)，說明必有兩個(gè)失敗結(jié)點(diǎn)所對應(yīng)的子句可做歸結(jié) ,將歸結(jié)式放入 S，就使 T倒塌。重復(fù)這個(gè)過程直到語義樹僅由樹根組成為止。樹根若是失敗結(jié)點(diǎn)， I(N0)= φ ，必然是已歸結(jié)出空子句口所致。 Herbrand定理 ?定理 1： 子句集 S是不可滿足的，當(dāng)且僅當(dāng)對應(yīng)于 S的完全語義數(shù)是棵有限封閉樹。 ?定理 2： 子句集 S是不可滿足的，當(dāng)且僅當(dāng)存在不可滿足的 S的有限基例集。 ?定理的意義 ： 將一階邏輯證明問題轉(zhuǎn)化成了有限的命題邏輯問題。此定理保證，可以放心的用機(jī)器來實(shí)現(xiàn)自動(dòng)推理了。（歸結(jié)原理） ?注意： Herbrand定理給出了一階邏輯的半可判定算法，即僅當(dāng)被證明定理是成立時(shí)，使用該算法可以在有限步得證。而當(dāng)被證定理并不成立時(shí)，使用該算法得不出任何結(jié)論。 結(jié)束語 ?使用 Herbrand定理，來證明定理或 S是不可滿足的，或是尋找有限的封閉樹，或是尋找有限的不可滿足的基例集。 ?重點(diǎn) ： 1． 這里公式 G的解釋的意義是：公式 G的一個(gè)解釋就是公式 G在其論域上的一個(gè)實(shí)例化。 2． H域?qū)嶋H上是對于論域的一種簡化。使得我們在一個(gè)能夠把握的論域中對邏輯命題進(jìn)行永假的判斷。 3． 以下的概念需要特別注意和區(qū)分： f(tn), 原子集，H解釋，基例。 ?仍然存在問題。 【 章節(jié)小結(jié) 】 ?本章敘述了命題邏輯的歸結(jié)法基礎(chǔ)。描述了將一個(gè)謂詞邏輯公式化為 Skolem標(biāo)準(zhǔn)形，得到相應(yīng)的子句集的方法。介紹了歸結(jié)法的一般過程，指出合一和置換是針對謂詞邏輯歸結(jié)的最重要的概念之一。并介紹了歸結(jié)法的策略控制。 ?從 Herbrand定理的有關(guān)內(nèi)容可知， Herbrand定理是歸結(jié)法的基礎(chǔ)。雖然通過構(gòu)造在 H域上的語法樹來判斷一個(gè)謂詞邏輯命題是否為永真，從而實(shí)現(xiàn)了將謂詞邏輯轉(zhuǎn)化成為命題邏輯判定問題，為 Herbrand定理提供了實(shí)現(xiàn)的途徑。最終還是歸結(jié)原理使Herbrand定理成為現(xiàn)實(shí)可用的。 演講完畢，謝謝觀看！