【正文】 |I=T， 就必有 S|I*=T。 證明 充分性 ：若 S在一般域 D上是不可滿足的 ， 必然在 H域上是不可滿足的 ， 從而對 H域上的一切解釋都為假 。 否則 ， 如果存在一個(gè)解釋 I0使 S為真 ， 那么依據(jù)定理 ，一定可以在 H域找到相對應(yīng)的一個(gè)解釋 I*0使 S為真 。 歸結(jié)推理方法 定理 子句集 S不可滿足的充分必要條件是存在一個(gè)有限的不可滿足的基例集 S′ 。 證明 充分性： 設(shè)子句集 S有一個(gè)不可滿足的基例集 S′ ， 因?yàn)樗豢蓾M足 ， 所以一定存在一個(gè)解釋 I′ 使 S′ 為假 。 歸結(jié)推理方法 必要性： 設(shè)子句集 S不可滿足 ， 由定理 ， S對 H域上的所有解釋均為假 。 既然至少有一個(gè)基例 Ci′ 為假 ， 因而 S的基例集 S′ 是不可滿足的 。 歸結(jié)推理方法 歸結(jié)原理 定義 若 P是原子謂詞公式或原子命題 ， 則稱 P與～ P為 互補(bǔ)文字 。 歸結(jié)推理方法 定理 歸結(jié)式 C12是其親本子句 C1和 C2的邏輯結(jié)論 。 如果把C12加入子句集 S后得到新子句集 S1， 則 S1和 S在不可滿足的意義下是等價(jià)的 。 (2) 將歸結(jié)所得的歸結(jié)式放入子句集 S中 ， 得新子句集 S′。否則轉(zhuǎn) （ 4） 。 歸結(jié)推理方法 2． 一階謂詞邏輯中的歸結(jié)原理 下面是謂詞邏輯關(guān)于歸結(jié)的定義 。 為了說明的方便 。 在集合的表示下做減法或做并運(yùn)算 ， 然后再寫成子句形 ， 如集合運(yùn)算結(jié)果為 {P(x),～ Q(y)}， 可改寫為 P(x)∨ ～ Q(y)。 從而沒有辦法進(jìn)行歸結(jié) 。 （ 3） 如果在參加歸結(jié)的子句內(nèi)含有可合一的文字 ， 則在進(jìn)行歸結(jié)之前 ，應(yīng)對這些文字進(jìn)行合一 ， 以實(shí)現(xiàn)這些子句內(nèi)部的化簡 。 定義 設(shè) C1和 C2是沒有相同變元的子句 ， 則下列四種二元?dú)w結(jié)式都叫做 C1和 C2的歸結(jié)式 ， 仍記作 C12。 （ 2） C1的因子 C1σ1與 C2的二元?dú)w結(jié)式 。 （ 4） C1的因子 C1σ1與 C2的因子 C2σ2的二元?dú)w結(jié)式 。解 若選 L1=～ P(a)， L2=P(y)， 則 L1和 L2的 mgu是 σ={a/y}， 于是由定義 C1和 C2 的二元?dú)w結(jié)式為 C12 =( C1σ{L1σ})∪ (C2 σ{L2σ}) =({～ P(a),Q(x),R(x)}{～ P(a)})∪ ({P(a),～ Q(b)}){P(a)} =({Q(x),R(x)})∪ ({～ Q(b)}) =Q(x)∨ R(x)∨ ～ Q(b) 若選 L1=Q(x)， L2=～ Q(b)， 則二者的 mguσ={b/x}， C12 =～ P(a)∨ R(b)∨ P(y) 歸結(jié)推理方法 3． 歸結(jié)原理的完備性 對于一階謂詞邏輯 ， 從不可滿足的意義上說 ， 歸結(jié)原理是完備的 。 歸結(jié)推理方法 利用歸結(jié)原理進(jìn)行定理證明 應(yīng)用歸結(jié)原理進(jìn)行定理證明的步驟如下： 設(shè)要被證明的定理可用謂詞公式表示為如下的形式： A1∧ A2∧ … ∧ An→ B (1) 首先否定結(jié)論 B， 并將否定后的公式～ B與前提公式集組成如下形式的謂詞公式： G= A1∧ A2∧ … ∧ An∧ ～ B (2) 求謂詞公式 G的子句集 S。 這就說明對結(jié)論 B的否定是錯(cuò)誤的 ， 推斷出定理的成立 。 證明 首先將 A和～ B化為子句集 (1) ～ P(x,y)∨ ～ Q(y) ∨ R(f(x)) (2) ～ P(x,y)∨ ～ Q(y) ∨ T(x,f(x)) //(1)(2)為 A (3) ～ R(z) (4) P(a， b) (5) Q(b) //(3)(4)(5)為 B 歸結(jié)推理方法 下面進(jìn)行歸結(jié)： （ 6） ～ P(x,y)∨ ～ Q(y) （ 1） 與 （ 3） 歸結(jié) ， σ={f(x)/z} （ 7） ～ Q(b) （ 4） 與 （ 6） 歸結(jié) ， σ={a/x,b/y} （ 8） NIL（ 空子句 ） （ 5） 與 （ 7） 歸結(jié) 所以 B是 A的邏輯結(jié)論 。 （ 2） 把待求解的問題也用謂詞公式表示出來 ， 然后將其否定 ， 并與一謂詞 ANSWER構(gòu)成析取式 。 （ 3） 把問題公式與謂詞 ANSWER構(gòu)成的析取式化為子句集 ， 并把該子句集與 S1合并構(gòu)成子句集 S。 （ 5） 如果得到歸結(jié)式 ANSWER ， 則問題的答案即在ANSWER謂詞中 。 （ 1） 定義謂詞： 設(shè) Father(x,y)表示 x是 y的父親 。 歸結(jié)推理方法 （ 2） 將已知事實(shí)用謂詞公式表示出來 。 (x)(y)(z)(Brother(x,y)∧ Father(z,x)→ Father(z,y)) F2： John和 Peter是兄弟 。 Father(David, John) （ 3） 將它們化成子句集得： S1={~Brother(x,y)∨ ~Father(z,x)∨ Father(z,y), Brother(John,Peter), Father(David,John)} 歸結(jié)推理方法 第二步：把問題用謂詞公式表示出來 ， 并將其否定與謂詞ANSWER作析取 。 將其否定與 ANSWER作析取 ， 得： G：～ Father(u,Peter)∨ ANSWER(u) 歸結(jié)推理方法 第三步：將上述公式 G化為子句集 S2， 并將 S1和 S2合并到 S。 （ 2） Brother(John,Peter)。 （ 4） ～ Father(u,Peter)∨ ANSWER(u)。 即 Peter的父親是 David。 由于事先并不知道子句集中的哪兩個(gè)子句可以進(jìn)行歸結(jié) ，也不知道通過對哪些子句的歸結(jié)可盡快得到空子句 ， 所以就必須對子句集中的所有子句逐一進(jìn)行比較 ， 以對所有可能歸結(jié)的子句對進(jìn)行歸結(jié) ，并將歸結(jié)式加入 S中 ， 再做第二層這樣的歸結(jié) ?? ， 直到產(chǎn)生空子句（ NIL） 為止 。 歸結(jié)推理方法 為了解決這一問題 ， 研究如何選擇合適的子句進(jìn)行歸結(jié) ， 以避免多余的 、 不必要的歸結(jié)式的出現(xiàn) ， 已顯得非常重要 。 歸結(jié)推理方法 2． 控制策略的分類 歸結(jié)策略大致可分為兩大類：一類是刪除策略 ， 刪除策略包括：純文字刪除法 、 重言式刪除法 、 包孕刪除法 。 包括：線性歸結(jié)策略 、 單元 （ 單文字 ） 歸結(jié)策略 、 輸入歸結(jié)策略 、 支持集策略等 。 例如 ， 設(shè)有子句集 ， S={T∨ Q∨ R,～ R,Q,R∨ ～ Q} 其中 T是純文字 ， 因此可將子句 T∨ Q∨ R刪去 ， 只用剩余的子句集進(jìn)行歸結(jié) ， 不會(huì)影響 S的不可滿足性 。 例如 ， Q(x)∨ ～ Q(x)， P(x)∨ ～ Q(x)∨ ～ P(x)都是重言式 。 可以從子句集中刪去重言式 。 例如 ， P(x)∨ Q(a)包孕于 P(f(a))∨ Q(a)∨ R(y) ， σ={f(a)/x} T(x)∨ S(y)包孕于 T(b)∨ S(v)∨ R(x) ， σ={b/x， v/y}。 歸結(jié)推理方法 2． 線性歸結(jié)策略 線性歸結(jié)策略對參加歸結(jié)的子句提出如下限制：首先從子句集 S中先取一個(gè)稱作 頂子句 的子句 C0開始作歸結(jié)；其次是將歸結(jié)過程中所得到的歸結(jié)式 Ci立即同另一子句 Bi進(jìn)行歸結(jié) ， 得歸結(jié)式 Ci+1， 而 Bi是原子句集 S中的一個(gè)子句或是已經(jīng)歸結(jié)出的某個(gè)歸結(jié)式 Cj（ ji） 。 如果在歸結(jié)過程中 ， 每次歸結(jié)都有一個(gè)子句是單文字子句 ， 則稱這種歸結(jié)就是 單文字歸結(jié) 。 這有利于朝著空子句的方向前進(jìn) ， 因此它有較高的歸結(jié)效率 。 因?yàn)榧僭O(shè)子句集 S是不可滿足的 ， 但其中卻不含有單文字子句 ， 則單元?dú)w結(jié)就無法進(jìn)行 。 5． 支持集策略 支持集策略對參加歸結(jié)的子句提出如下限制：每一次歸結(jié)時(shí) ， 參加歸結(jié)的兩個(gè)子句中至少應(yīng)有一個(gè)是由目標(biāo)公式的否定所得到的子句 ， 或者是它們的后裔