【正文】 上述每個路徑所代表的解釋已經(jīng)使 S的某個子句為假 ， 因此再擴充路徑仍然只能使同一子句為假 ， 所以沒有擴充 、 延伸的必要 □ 第 4章 消解法 30 有限封閉語義樹 ? 上例說明 ， 從不可滿足的角度來說 ， 對于無限完備語義樹只需搜索到一個否節(jié)點 ，則該分枝即被證明為不可滿足 。設(shè) B是 T的任意一個分支路徑，則 IB是對應該分支上 S的一個解釋 由 S的不可滿足性知 IB使 S的某子句的某個基例為假。 因為 T是二叉樹且每個節(jié)點只有兩個子節(jié)點，由 B的任意性可知， T所有分支上的否節(jié)點所構(gòu)成的封閉語義樹必是有限的。設(shè) I是S的任一解釋，則其落在 T的某個分支 B上， B上必有否節(jié)點 N存在 可知 I(N)使 S的某子句的某個基例 C’為假。由 Herbrand定理 I知存在 T的有限封閉子樹 T’。 將基例加起來，即得一 個不可滿足的有限基例集 第 4章 消解法 34 Herbrand定理 II(2) ? [必要性 ]設(shè) S’?S且不可滿足的有限基例集。 經(jīng)過如此處理的子句集為 S’， 若 S’為空 ， 則 S是可滿足的 ， 若 S’非空 ， 則 S’與 S同是不可滿足的； (3)純文字刪除規(guī)則：如果 S中只包含文字 L而不包含 ﹁ L， 則刪去所有包含 L的子句； 第 4章 消解法 37 DavisPutnam預處理 (2) (4)分離規(guī)則 (分裂規(guī)則 )：如果 S=(L∨ A1)∧ … ∧ (L∨ Am)∧ (﹁ L∨ B1)∧ … ∧ (﹁ L∨ Bn)∧ R 其中 Ai、 Bj、 R皆不包含 L或 ﹁ L，則令 S1= A1∧ … ∧ Am∧ R S2= B1∧ … ∧ Bn∧ R S是不可滿足的等價于 S1∨ S2是不可滿足的 (即 SS2同時不可滿足 )。 例如設(shè) ? 此時只要使用單文字刪除規(guī)則就可以推出結(jié)論 Q。置換 θ={t1/x1, t2/x2 …t n/xn}作用于謂詞公式 E就是將 E中變量 xi均以 ti代替，其結(jié)果用 E?表示 / 作用于項的含義相同 第 4章 消解法 41 關(guān)于置換 ? 例： ?={a/x, f(b)/y, u/z} E=P(x, y, z) t=g(x, y) E?=P(a, f(b), u) t?=g(a, f(b)) ? [定義 ]置換乘積 (合成 )：設(shè) ?和 ?是 2個置換 ， 則先 ?后 ?作用于公式或項 ， 稱為置換乘積 ， 用 ???表示 (E???) ? 一般來說 ， 置換乘積的結(jié)合律成立 ，即 (???)??=??(???)， 但交換律不成立 第 4章 消解法 42 合一置換 ? [定義 ]合一置換：設(shè)有一組謂詞公式 {E1～Ek}和置換 ?，使 E1?=E2?=…=E k?， 則 ?稱為合一置換， E1～ Ek稱為可合一的。 ? 分歧集性質(zhì)：分歧集的出現(xiàn)處一定是謂詞或項的開始處 / 求最廣合一置換只考察項的分歧 第 4章 消解法 44 mgu求解算法 ? 求 mgu算法 (合一算法 ) ? 設(shè) W是謂詞組 ， ? 表示空置換 (即置換序列為空 )， 則算法如下： (1)k=0， W0=W， ?0=?； (2)如果 Wk中各謂詞完全一樣 ， 則算法結(jié)束 ， ?k是 W的mgu， 否則求 Wk的分歧集 Dk； (3)若 Dk含變量 x k以及項 t k的首符號且 x k在 t k中不出現(xiàn) ，則繼續(xù)執(zhí)行算法 ， 否則 W的 mgu不存在 ， 算法停止； (4)令 ?k+1=?k?{t k/x k}， Wk+1= Wk{t k/x k}； (5)k=k+1， 轉(zhuǎn) (2) 第 6章 消解法 45 mgu存在條件 ? mgu存在的條件：如果有限謂詞組 W是可合一的，則上述算法一定成功結(jié)束并給出其存在 ? 求 mgu的預置條件：應把所有謂詞中的變量換成不同名字的變量 。 ) 第 4章 消解法 46 mgu求解例子 (1) ? 例 1：求 W={P(a, x, f(g(y))), P(z, f(a), f(u))}的mgu (1)?0=?， W0=W， D0={a, z} (2)?1=?0?{a/z}={a/z}， W1= W0?1={P(a, x, f(g(y))), P(a, f(a), f(u))}， D1={x, f(a)} (3)?2=?1?{f(a)/x}={a/z, f(a)/x}， W2= W1?2= {P(a, f(a), f(g(y))), P(a, f(a), f(u))}， D2={g(y), u} (4)?3=?2?{g(y)/u}={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)))}, D3=? 此時 W已合一 ， mgu=?3={a/z, f(a)/x, g(y)/u} ★ 第 4章 消解法 47 mgu求解例子 (2) ? 例 2：求 W={P(x, x), P(x, f(x))}的 mgu 首先換名： W={P(x, x), P(y, f(y))} (1)?0=?， W0=W， D0={x, y} (2)?1={x/y}， W1={P(x, x), P(x, f(x))}， D1={x, f(x)} (3)?2不存在 ， 因為 f(x)中含有變量 x。 ★ 第 4章 消解法 48 消解式 ? [定義 ]文字合并規(guī)則：若子句 C含有 n(n1)個相同的文字 (也稱為句節(jié) )， 則刪去其中的n1個 ， 結(jié)果以 [C]表示 。 當 [C?]為單文字時稱為 C的單因子 ? 通過取因子可以簡化一個子句 。 L1和 L2稱為被消解的文字， C C2稱為父子句 第 4章 消解法 50 二元消解式例子 ? 例子： 設(shè) C1=P(x)∨ Q(x), C2=?P(g(y))∨ ?Q(b)∨ R(x)，則 C1和 C2有 2個二元消解式 (一個消 P，一個消 Q) 如果取 ?={g(y)/x}，得 R(C1, C2)=Q(g(y))∨ ?Q(b)∨ R(g(y)) 如果取 ?={b/x}，得 R(C1, C2)=P(b)∨ ?P(g(y))∨ R(b) ★ ? 注意：求消解式不能同時消去 2個互補對文字，如同時消去 P和 ?P、 Q和 ?Q，那樣所得結(jié)果就不是 C1, C2的邏輯結(jié)果了 第 4章 消解法 51 子句的二元消解式 ? 子句的二元消解式：以下 4種二元消解式都是子句 C1和 C2的二元消解式： (1)C1和 C2的二元消解式； (2)C1的一個因子 (即經(jīng)過取因子處理 )和 C2的二元消解式； (3)C1和 C2的一個因子的二元消解式； (4)C1的一個因子和 C2的一個因子的二元消解式 第 4章 消解法 52 消解法的實施 ? 消解法的實施：為證 ├A→B ， 則建立G=A∧ ﹁ B(﹁ (A→B)) ， 再求出 G對應的子句集 S， 進而只需證明 S是不可滿足的 ? 為證 S的不可滿足 ， 只要對 S中可以消解的子句求消解式 ， 并將消解式 (新子句 )加入 S中 ， 反復進行這樣的消解過程直到產(chǎn)生一個空子句 □ 第 4章 消解法 53 子句的推導 ? 子句的推導定義： ? 給定子句集 S， 如果存在一個有限的子句序列 C1,C2,… ,Ck， 使得每個 Ci或者屬于 S，或者是 C1～Ci1的某些子句的消解式 ， 且Ck=C， 則從 S可以推導出子句 C， 稱此子句序列為 C的推導 。 第 4章 消解法 54 消解法的合理性 ? [合理性定理 ]若從子句集 S可以推導出子句 C，則 C是 S的邏輯推論 (或 S邏輯蘊含 C)。 ? 其逆否形式：若 S推導出空子句□，則 S是不可滿足的。即只要找出一個推出空子句的過程，則 S就不可滿足 第 4章 消解法 55 消解法的完備性 (1) ? [完備性定理 ]子句集 S是不可滿足的，當且僅當從 S可推導出空子句□ ? 為了說明完備性定理的證明過程，需要說明 消解過程與語義樹倒塌之間的聯(lián)系： ? 從 S的語義樹 T出發(fā)，必有兩個否節(jié)點所對應的子句可作歸結(jié)，將歸結(jié)式放入 S，則否節(jié)點的位置提升，即原來兩個否節(jié)點的父節(jié)點成為否節(jié)點。此時樹根是否節(jié)點，則 I(N0)= ?，即已歸結(jié)為空子句 □。P∨ Q, 172。Q} 第 4章 消解法 T N 0 T * N 0 T *1 N 0 P 172。 P N 11 N 12 N 11 N 12 N 11 N 12 Q 172。 Q N 21 N 22 N 23 N 24 N 21 N 2257 提升引理 ? 歸結(jié)過程與語義樹的倒塌過程是一致的 ? 進一步推廣：由基例間 (語義樹對應的形式 )可作歸結(jié)，到實現(xiàn)子句間可作歸結(jié)：即常量子句到變量子句的歸結(jié) / 于是得到提升引理 ? [提升引理 ]若 C1’和 C2’分別是子句 C1和 C2的例子句， C’是 C1’和 C2’的歸結(jié)式，則存在 C1和 C2的一個歸結(jié)式 C，使得 C’是 C的例子句 第 4章 消解法 58 消解法完備性定理 (1) ? 簡述完備性定理的證明過程： (1)必要性：存在 S到□的歸結(jié)過程，□是 S的邏輯推論，由合理性定理知 S是不可滿足的 (2)充分性： S不可滿足，由 Herbrand定理知存在有限封閉語義樹，必有二叉樹中 2個兄弟節(jié)點均為否節(jié)點，即使某 2個 S的基例為假 該 2個基例必可作歸結(jié) (有互補原子 )，則歸結(jié)式使其父節(jié)點成為否節(jié)點 (使歸結(jié)式為假 ) 第 4章 消解法 59 消解法完備性定理 (2) ? 將歸結(jié)式并入