【正文】 言式刪除規(guī)則也說明了這一點 。 如果限定消解雙方不能都取自S―S’ ， 則此消解稱為支持集消解 ? 給定 S’之后 ， 若每一步消解都是支持集消解 ，則此推導(dǎo)稱為支持集推導(dǎo) ， 其結(jié)果為空子句時稱為支持集否證 。 ? 例 2： S={ P∨ Q,﹁ P∨ Q, P∨ ﹁ Q, ﹁ P∨ ﹁ Q }，其線性消解過程可由下圖說明 。 ? [定理 ]輸入消解和單元消解對于 Horn子句集都是完備的 第 4章 消解法 79 有序消解策略 ? 有序消解策略：對子句中被消解的文字加以限制 (第 2種策略 )，通常要對子句中的文字進(jìn)行排序。 第 4章 消解法 84 第 4章 消解法 解 ：先將問題謂詞表示如下： “任何通過計算機考試并獲獎的人都是快樂的” ?( )(x ),( c o m p u te rxP a ss ))()),( xH a p p yp rizexW in ?? “任何肯學(xué)習(xí)或幸運的人 都可以通過所有考試” ?( ?)(x )()( xS tu d yy ? )),()() yxP a ssxLu c ky ? “張不肯學(xué)習(xí)但他是幸運的” ￢ )( zh a n gS tu sy )( zh a n gLu c ky? “張不肯學(xué)習(xí)但他是幸運的” ?( )(x L uck y )( x )),( p rizexW in? 結(jié)論“張是快樂的”的否定 ￢ )( zh a n gH a p p y 85 第 4章 消解法 將上述謂詞公式轉(zhuǎn)化為子句集如下： (1) ￢ ?),( c o m p u terxP a ss ￢ )(),( xHa p p yp r izexW in ? (2) ￢ ),()( zyP a ssyS tu d y ? (3) ￢ ),()( vuP a ssuLu c ky ? (4) ￢ )( zh a n gS tu d y (5) )( zh a n gLu c ky (6) ￢ ),()( p r izewW inwLu c k y ? (7) ￢ )( zh a n gH a p p y ( 本子句為結(jié)論的否定 ) 按謂詞邏輯的歸結(jié)原理對此子句進(jìn)行歸結(jié)，其歸結(jié)反演過程如 下 圖 所示。 ? [簡單語義消解定義 ]設(shè) HI是子句集 S的一個 H解釋， Sn(n=0, 1, …) 定義如前， Sn1和 Sn2分別為 HI解釋中取真值和假值的子句集。 ★ 第 4章 消解法 S2 ﹁ R ○ ○﹁ Q ∨ R ﹁ Q ○ ○ P ∨ Q P ○ ○﹁ P ∨ R R ○ ○﹁ R □ ○78 輸入消解和單元消解的關(guān)系 ? 可以證明如下定理：輸入消解和單元消解是等價的，即一個子句集 S可以用輸入消解來否證，當(dāng)且僅當(dāng) S可以用單元消解來否證。支持集消解的進(jìn)一步改進(jìn)就得到了動態(tài)支持集消解 ? [定義 ]動態(tài)支持集消解：設(shè) S是子句集， S0=S，Sn=Sn1 ∪ {Cn}，其中 Cn是 Sn中兩個子句的消解式，如果有一種根據(jù)子句的語法結(jié)構(gòu)劃分子句集的統(tǒng)一方法，使每個 Sn都劃分為 Sn1和 Sn2兩部分，且在消解時限定雙方不能都取自 Sn1 ，則稱 Sn2是 Sn的一個動態(tài)支持集，此消解稱為動態(tài)支持集消解。 ★ 第 4章 消解法 69 禁止無用子句產(chǎn)生 ? 禁止無用子句的產(chǎn)生：刪去重言式和被隱含子句的策略提示我們，如果不讓無用子句產(chǎn)生，其效率會更高。 Q N 21 N 22 N 23 N 24 N 21 N 2257 提升引理 ? 歸結(jié)過程與語義樹的倒塌過程是一致的 ? 進(jìn)一步推廣：由基例間 (語義樹對應(yīng)的形式 )可作歸結(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é)式并入 S，則該父節(jié)點是并集的否節(jié)點，因此引起語義樹的倒塌 ? 重復(fù)上述過程至語義樹倒塌為只剩根節(jié)點且為否節(jié)點，說明 S∪ {R’,...}有限集必包含□。此時樹根是否節(jié)點，則 I(N0)= ?，即已歸結(jié)為空子句 □。 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對應(yīng)的子句集 S， 進(jìn)而只需證明 S是不可滿足的 ? 為證 S的不可滿足 ， 只要對 S中可以消解的子句求消解式 ， 并將消解式 (新子句 )加入 S中 ， 反復(fù)進(jìn)行這樣的消解過程直到產(chǎn)生一個空子句 □ 第 4章 消解法 53 子句的推導(dǎo) ? 子句的推導(dǎo)定義： ? 給定子句集 S， 如果存在一個有限的子句序列 C1,C2,… ,Ck， 使得每個 Ci或者屬于 S，或者是 C1～Ci1的某些子句的消解式 ， 且Ck=C， 則從 S可以推導(dǎo)出子句 C， 稱此子句序列為 C的推導(dǎo) 。 ? 分歧集性質(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的預(yù)置條件：應(yīng)把所有謂詞中的變量換成不同名字的變量 。 將基例加起來，即得一 個不可滿足的有限基例集 第 4章 消解法 34 Herbrand定理 II(2) ? [必要性 ]設(shè) S’?S且不可滿足的有限基例集。設(shè) B是 T的任意一個分支路徑，則 IB是對應(yīng)該分支上 S的一個解釋 由 S的不可滿足性知 IB使 S的某子句的某個基例為假。 對 i≥1令 Hi=Hi1∪ {f(t1,… tn)| n≥1 f 是 S中的任一函數(shù)符號 ， t1,… tn是 Hi1中的元素 則 Hi 稱為 S的 i階常量集 ， H∞稱為 S的 Herbrand論域 ，其元素稱為基項 。 ? 合取范式：形如 A1∧ A2∧ … ∧ An的公式 ， 其中 A1～ An均為子句 。下圖中語義樹和前圖中的語義樹對應(yīng)于同一個 H基 。由I(N)?I及任意性，可知 S是不可滿足的 ★ 第 4章 消解法 33 Herbrand定理 II(1) ? Herbrand定理 II： S是不可滿足的，當(dāng)且僅當(dāng)存在 S的一個不可滿足的有限基例集 ? 證明： ? [充分性 ]設(shè) S是不可滿足的，及 T是 S的一個完備語義樹。 但是如果子句中包含變量 ， 則常常必須經(jīng)過變量置換才能進(jìn)行消解 ? 本節(jié)的內(nèi)容：置換與合一 / 合一算法 / 子句化簡與消解式 / 消解法實施 / 消解法合理性和完備性 第 4章 消解法 ?????? QPPS40 置換與合一 ? [定義 ]置換 (或代換 )：設(shè) x1～ xn是 n個變量，且各不相同， t1～ tn是 n個項 (常量、變量、函數(shù) )， ti≠xi，則有限序列 {t1/x1, t2/x2 …t n/xn}稱為一個置換 ? 置換可以作用于謂詞公式，也可以作用于項。 ? [定義 ]因子：若子句 C中的多個文字具有mgu， 則 [C?]稱為 C的一個因子 。 ? 此為消解原理的合理性定理。 P P 1