【正文】 而 {P(a),Q(a)}的邏輯表示就是 D=P(a)∨ Q(a)。 于是 C把 D歸類 。 ? 刪除策略 =完備。 （采用歸結(jié)策略進(jìn)行的歸結(jié)過程沒有破壞歸結(jié)法的完備性。） 采用支撐集策略 名詞解釋 ： 支撐集 ：設(shè)有不可滿足子句集 S的子集 T，如果 ST是可滿足的，則 T是支持集。 ? 采用支撐集策略時，從開始到得到 ?的整個歸結(jié)過程中，只選取不同時屬于 ST的子句，在其間進(jìn)行歸結(jié)。就是說，至少有一個子句來自于支撐集 T或由 T導(dǎo)出的歸結(jié)式。 ? 例如： A1∧ A2∧ A3∧ ～ B中的～ B可以作為支撐集使用。要求每一次參加歸結(jié)的親本子句中，只要有一個是有目標(biāo)公式的否定（～ B）所得到的子句或者它們的后裔。 ? 支撐集策略的歸結(jié)是完備的。同樣，所有可歸結(jié)的謂詞公式都可以用采用支撐集策略達(dá)到加快歸結(jié)速度的目的。問題是如何尋找合適的支撐集。一個最容易找到的支撐集是目標(biāo)子句的非，即 S～ B。 支持集策略的語義歸結(jié)過程 例 S={P ∨ Q,～ P ∨ R,～ Q ∨ R,～ R} 取 T={～ R} 支持集歸結(jié)過程： (1)P ∨ Q (2)～ P∨ R (3)～ Q ∨ R (4)～ R (5)～ P (2)(4) (6)～ Q (3)(4) (7)Q (1)(5) (8)口 (6)(7) 語義歸結(jié)策略 ? 語義歸結(jié)策略是將子句 S分成兩部分 ， 約定每部分內(nèi)的 子句間不允許做歸結(jié) 。 還引入了文字次序 ， 約定歸結(jié)時其中的一個子句的被歸結(jié)文字只能是該子句中 “ 最大 ” 的文字 。 例 S={～ P∨ ～ Q∨R,P∨R,Q∨R, ～ R} 1）規(guī)定 S中出現(xiàn)的文字的次序為 PQR。 2） 選取 S的一個解釋 I=(～ P,～ Q,～ R)用它來將 S 分成兩個部分 。 S1’={P∨R,Q∨R} 為在 I下為假的子句集合 S2’={ ～ P∨ ～ Q∨R, ～ R}為在 I下為真的子句集合 規(guī)定 Si’ 內(nèi)部的子句不允許歸結(jié) , S1’ 與 S2’ 子句間的歸結(jié)必須是 S1’ 中的最大文字方可進(jìn)行 。 這樣所得的歸結(jié)式 ,仍按 I來放入 S1’ 或 S2’ 。 3）歸結(jié)過程： (1)～ P∨ ～ Q∨ R ∈ S2? (2)P∨ R ∈ S1? (3)Q∨ R ∈ S1? (4)～ R ∈ S2? (5)～ Q∨ R (2)(1)歸結(jié) ∈ S2? (6)～ P∨ R (3)(1)歸結(jié) ∈ S2? (7)R (2)(6)歸結(jié) ∈ S1? (8)R (3)(5)歸結(jié) ∈ S1? (9)口 (7)(4)歸結(jié) 線性歸結(jié)策略 線性歸結(jié) ? 完備 圖 2－ 5 線性歸結(jié)策略示意圖 ? 線性歸結(jié)策略首先從子句集中選取一個稱作 頂子句 的子句 C0開始作歸結(jié)。歸結(jié)過程中所得到的歸結(jié)式 Ci立即同另一子句 Bi進(jìn)行歸結(jié)得歸結(jié)式 Ci+1 。而 Bi屬于 S或是已出現(xiàn)的歸結(jié)式 Cj (ji)。即，如圖所示歸結(jié)得到的新子句立即參加歸結(jié)。 ? 線性歸結(jié)是完備的。同樣，所有可歸結(jié)的謂詞公式都可以采用線性歸結(jié)策略達(dá)到加快歸結(jié)速度的目的。如果能搞找到一個較好的頂子句，可以使歸結(jié)順利進(jìn)行。否則也可能事與愿違。 例 S={P ∨ Q，～ P ∨ Q， P ∨ ～ Q， ～ P∨ ～ Q} 選取頂子句 Co=P∨ Q 線性歸結(jié)過程 : (l)P∨Q (2)～ P∨Q (3)P∨ ～ Q (4)～ P∨ ～ Q (5)Q (1)(2) (6)P (5)(3) (7)～ Q (6)(4) (8)口 (7)(5) 單元歸結(jié)策略 ?單元歸結(jié)策略要求在歸結(jié)過程中，每次歸結(jié)都有一個子句是單元子句（只含一個文字的子句）或單元因子。顯而易見，詞中方法可以簡單地削去另一個非單子句中的一個因子，使其長度減少，構(gòu)成簡單化，歸結(jié)效率較高。 ? 單元歸結(jié) ? 完備；反之不成立。 ?初始子句集中沒有單元子句時，單元歸結(jié)策略無效。所以說 反之不成立 ，即此問題不能采用單元歸結(jié)策略。 單元歸結(jié)的例子 例 1 S={P ∨ Q,～ P ∨ R,～ Q ∨ R,～ R} 單元歸結(jié)過程 (1)P∨ Q (2)～ P∨ R (3)～ Q∨ R (4)～ R (5)～ P (4)(2) (6)～ Q (4)(3) (7)Q (5)(1) (8)P (6)(1) (9)R (7)(3) (10)口 (7)(6) 輸入歸結(jié)策略 ? 與單元歸結(jié)策略相似，輸入歸結(jié)策略要求在歸結(jié)過程中，每一次歸結(jié)的兩個子句中必須有一個是 S的原始子句。這樣可以避免歸結(jié)出的不必要的新子句加入歸結(jié)，造成惡性循環(huán)?？梢詼p少不必要的歸結(jié)次數(shù)。 ? 輸入歸結(jié) ? 完備；反之不成立。 ? 如同單元歸結(jié)策略，不是所有的可歸結(jié)謂詞公式的最后結(jié)論都是可以從原始子句集中的得到的。簡單的例子，歸結(jié)結(jié)束時，即最后一個歸結(jié)式為空子句的條件是，參加歸結(jié)的雙方必須是兩個單元子句。原始子句集中沒有單元子句的謂詞公式一定不能采用輸入歸結(jié)策略。 例 2 S={P∨ Q,～ P∨ R,～ Q∨ R， ～ R} 輸入歸結(jié)過程 (1)P∨ Q (2)～ P∨ R (3)～ Q∨ R (4)～ R (5)Q∨ R (1)(2) (6)R (3)(5) (7)口 (4)(6) Herbrand定理 ?Herbrand定理是歸結(jié)原理的理論基礎(chǔ)，歸結(jié)原理的正確性是通過 Herbrand定理來證明的。同時歸結(jié)原理是Herbrand定理的具體實現(xiàn)，利用 Herbrand定理對公式的證明是通過歸結(jié)法來進(jìn)行的。本節(jié)簡單地描述了Herbrand定理的基本思想和相關(guān)預(yù)備知識，最后給出Herbrand定理的一般形式。 ?定義：公式 G永真：對于 G的所有解釋， G都為真。 ?定義：公式 G永假（矛盾）： 沒有一個解釋使 G為真。 Herbrand 定理概述 ?問題：一階邏輯公式的永真性（永假性）的判定是否能在有限步內(nèi)完成？ ?1936年圖靈 (Turing)和邱吉 (Church)互相獨立地證明了： “沒有一般的方法使得在有限步內(nèi)判定一階邏輯的公式是否是永真（或永假）。但是如果公式本身是永真（或永假）的，那么就能在有限步內(nèi)判定它是永真（或永假）。對于非永真（或永假）的公式就不一定能在有限步內(nèi)得到結(jié)論。判定的過程將可能是不停止的。 ” Herbrand 定理思想 ?要證明一個公式是永假的，采用反證法的思想（歸結(jié)原理），就是要尋找一個已給的公式是真的解釋。然而，如果所給定的公式的確是永假的，就沒有這樣的解釋存在，并且算法在有限步內(nèi)停止。 ?因為量詞是任意的，所討論的個體變量域 D是任意的，所以解釋的個數(shù)是無限、不可數(shù)的，要找到所有的解釋是不可能的。 ?Herbrand 定理的基本思想是簡化討論域，建立一個比較簡單、特殊的域，使得只要在這個論域上（此域稱為 H域），原謂詞公式仍是不可滿足的，即保證不可滿足的性質(zhì)不變。 H域 ?H域的定義： 設(shè) G是已給的公式 ,定義在論域 D上 ,令 H0是 G中所出現(xiàn)的常量的集合。若 G中沒有常量出現(xiàn) ,就任取常量 a∈D,而規(guī)定 H0={a}。 Hi=Hil∪{ 所有形如 f(t1,...,tn)的元素 } 其中 f(tl,? ,tn)是出現(xiàn)于 G中的任一函數(shù)符號 , 而 t1,? ,tn是 Hi1的元素 ,i=1,2,? 。 規(guī)定 H∞ 為 G的 H域 (或說是相應(yīng)的子句集 S的 H域 )。 ?不難看出， H域是直接依賴于 G的，而且最多只有可數(shù)個元素。 H域和 D域關(guān)系示意圖如下圖表示。 圖 2－ 1 H域與 D域關(guān)系 H域例題 ? 例題 24：設(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 ∪ ……… 解畢。 原子集 A ? 原子集 A為公式中出現(xiàn)的謂詞套上 H域的元素組成的集合。 A = {所有形如 P(t1,...,tn)的元素 }。 這里， P(x1,?,x n)為出現(xiàn)于 S中的任一謂詞符號，而 t1,...,tn為 S的 H域中的任意元素。即把 H域中的東西填到S的謂詞里去。 ? 上例題的原子集為： A = { P(a), Q(a, a), R(a), P(b), Q(b, a), Q(b, b), Q(b, a), 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(