【文章內(nèi)容簡介】 單文字子句 L(即只有一個原子公式 )， 則從 S中刪去所有含 L的子句 ， 從 S中刪去所有子句中的 ﹁ L文字 。 經(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同時不可滿足 )。經(jīng)過 DavisPutnam預處理以后的子句集與原子句集在不可滿足性上等價 第 4章 消解法 38 消解法 置換與合一 消解式 消解法的實施 第 4章 消解法 39 消解法的形式 ? 進一步推廣 DavisPutnam規(guī)則 ， 就得到了消解法 。 例如設 ? 此時只要使用單文字刪除規(guī)則就可以推出結論 Q。 但是如果子句中包含變量 ， 則常常必須經(jīng)過變量置換才能進行消解 ? 本節(jié)的內(nèi)容：置換與合一 / 合一算法 / 子句化簡與消解式 / 消解法實施 / 消解法合理性和完備性 第 4章 消解法 ?????? QPPS40 置換與合一 ? [定義 ]置換 (或代換 )：設 x1～ xn是 n個變量，且各不相同， t1～ tn是 n個項 (常量、變量、函數(shù) )， ti≠xi，則有限序列 {t1/x1, t2/x2 …t n/xn}稱為一個置換 ? 置換可以作用于謂詞公式，也可以作用于項。置換 θ={t1/x1, t2/x2 …t n/xn}作用于謂詞公式 E就是將 E中變量 xi均以 ti代替，其結果用 E?表示 / 作用于項的含義相同 第 4章 消解法 41 關于置換 ? 例： ?={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)) ? [定義 ]置換乘積 (合成 )：設 ?和 ?是 2個置換 ， 則先 ?后 ?作用于公式或項 ， 稱為置換乘積 ， 用 ???表示 (E???) ? 一般來說 ， 置換乘積的結合律成立 ，即 (???)??=??(???)， 但交換律不成立 第 4章 消解法 42 合一置換 ? [定義 ]合一置換：設有一組謂詞公式 {E1～Ek}和置換 ?，使 E1?=E2?=…=E k?， 則 ?稱為合一置換， E1～ Ek稱為可合一的。合一置換也叫通代 ? [定義 ]最一般合一置換 (最廣通代 )：如果 ? 和 ?都是公式組 {E1～ Ek}的合一置換，且有置換 ?存在，使得 ?=???，則 ?稱為公式組{E1～ Ek}的最一般合一置換，記為 mgu (most general unification) 第 4章 消解法 43 分歧集 ? 在介紹 mgu求解算法之前，首先說明什么是分歧集 / 合一的過程就是消除分歧 ? [定義 ]分歧集 (不一致集 )： 設 W是一個非空謂詞集，從左至右逐個比較 W中的符號，如果在第 i(i?1)個符號處 W中各謂詞第一次出現(xiàn)分歧(即至少存在 Ej和 Ek在第 i個符號處不一樣，而在i之前各謂詞符號均一樣 )，則全體謂詞的第 i個符號構成了 W的分歧集 D。 ? 分歧集性質：分歧集的出現(xiàn)處一定是謂詞或項的開始處 / 求最廣合一置換只考察項的分歧 第 4章 消解法 44 mgu求解算法 ? 求 mgu算法 (合一算法 ) ? 設 W是謂詞組 ， ? 表示空置換 (即置換序列為空 )， 則算法如下： (1)k=0， W0=W， ?0=?； (2)如果 Wk中各謂詞完全一樣 ， 則算法結束 ， ?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， 轉 (2) 第 6章 消解法 45 mgu存在條件 ? mgu存在的條件：如果有限謂詞組 W是可合一的，則上述算法一定成功結束并給出其存在 ? 求 mgu的預置條件：應把所有謂詞中的變量換成不同名字的變量 。 (不過 ， 這在將公式化為子句集時已經(jīng)完成 。 ) 第 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。 故 W的 mgu不存在 。 ★ 第 4章 消解法 48 消解式 ? [定義 ]文字合并規(guī)則：若子句 C含有 n(n1)個相同的文字 (也稱為句節(jié) )， 則刪去其中的n1個 ， 結果以 [C]表示 。 ? [定義 ]因子：若子句 C中的多個文字具有mgu， 則 [C?]稱為 C的一個因子 。 當 [C?]為單文字時稱為 C的單因子 ? 通過取因子可以簡化一個子句 。 這是因為取因子之后 ， 子句 C中可能出現(xiàn)相同的文字 ，而根據(jù)文字合并規(guī)則就可以刪除重復部分 第 4章 消解法 49 二元消解式 ? 例子： C=P(x, a)∨ P(b, y)∨ Q(x, y, c)， ?={b/x, a/y} 則 [C?]=[P(b, a)∨ P(b, a)∨ Q(b, a, c)]= P(b, a)∨ Q(b, a, c) ? [定義 ]二元消解式： 設 C C2是無公共變量的子句，分別含文字 L L2，而 L1和 ?L2有 mgu ?，則子句 R(C1, C2)=[(C1??L1?)∨ (C2??L2?)] 稱為 C1和 C2的二元消解式，其中 (C1??L1?)和 (C2??L2?)分別表示從 C1?、 C2?刪去 L1?、 L2?所余部分。 L1和 L2稱為被消解的文字， C C2稱為父子句 第 4章 消解法 50 二元消解式例子 ? 例子： 設 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，那樣所得結果就不是 C1, C2的邏輯結果了 第 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的推導 。 當 C為空子句 □ 時 ，也稱該序列為 S的一個否證 。 第 4章 消解法 54 消解法的合理性 ? [合理性定理 ]若從子句集 S可以推導出子句 C，則 C是 S的邏輯推論 (或 S邏輯蘊含 C)。 ? [推論 ]若 S是可滿足的，則 S推導出的任一子句也是可滿足的，即不能推出空子句。 ? 其逆否形式：若 S推導出空子句□，則 S是不可滿足的。 ? 此為消解原理的合理性定理。即只要找出一個推出空子句的