【正文】 這在將公式化為子句集時已經(jīng)完成 。 ) 第 4章 消解法 24 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章 消解法 25 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不存在 ， 因?yàn)?f(x)中含有變量 x。 故 W的 mgu不存在 。 ★ 第 4章 消解法 26 消解式 ? [定義 ]文字合并規(guī)則：若子句 C含有 n(n1)個相同的文字 (也稱為句節(jié) )， 則刪去其中的n1個 ， 結(jié)果以 [C]表示 。 ? [定義 ]因子：若子句 C中的多個文字具有mgu， 則 [C?]稱為 C的一個因子 。 當(dāng) [C?]為單文字時稱為 C的單因子 ? 通過取因子可以簡化一個子句 。 這是因?yàn)槿∫蜃又?， 子句 C中可能出現(xiàn)相同的文字 ，而根據(jù)文字合并規(guī)則就可以刪除重復(fù)部分 第 4章 消解法 27 ? 例子： 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) 28 二元消解式 ? [定義 ]二元消解式： 設(shè) 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章 消解法 29 二元消解式例子 ? 例子： 設(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個互補(bǔ)對文字，如同時消去 P和 ?P、 Q和 ?Q，那樣所得結(jié)果就不是 C1, C2的邏輯結(jié)果了 第 4章 消解法 30 子句的二元消解式 ? 子句的二元消解式：以下 4種二元消解式都是子句 C1和 C2的二元消解式： (1)C1和 C2的二元消解式； (2)C1的一個因子 (即經(jīng)過取因子處理 )和 C2的二元消解式； (3)C1和 C2的一個因子的二元消解式； (4)C1的一個因子和 C2的一個因子的二元消解式 第 4章 消解法 31 消解法的實(shí)施 ? 消解法的實(shí)施：為證 ├A→B ， 則建立G=A∧ ﹁ B(﹁ (A→B)) ， 再求出 G對應(yīng)的子句集 S， 進(jìn)而只需證明 S是不可滿足的 ? 為證 S的不可滿足 ， 只要對 S中可以消解的子句求消解式 ， 并將消解式 (新子句 )加入 S中 ， 反復(fù)進(jìn)行這樣的消解過程直到產(chǎn)生一個空子句 □ 第 4章 消解法 32 消解的注意事項(xiàng) ? 1. 謂詞的一致性， P( )與 Q( )，不可以 ? 2. 常量的一致性， P(a,…) 與 P(b,…) ，不可以；但是 P(a,…) 與 P(x,…) ，可以 ? 3. 變量與函數(shù)， P(a, x,…) 與 P(x, f(x),…) ，不可以；但是 P(a, x,…) 與 P(x, f(y)…) ，可以 ? 4. 不能同時消去兩個互補(bǔ)對 ? 5. 先進(jìn)行內(nèi)部簡化（置換、合并） 33 消解法舉例 ? “快樂學(xué)生 ” 問題 ? 假設(shè)：任何通過計(jì)算機(jī)考試并獲獎的人都是快樂的 ， 任何肯學(xué)習(xí)或幸運(yùn)的人都可以通過所有考試 ， 張不肯學(xué)習(xí)但他是幸運(yùn)的 ， 任何幸運(yùn)的人都能獲獎 。 求證：張是快樂的 。 ? 證明過程：所有假設(shè)表示為一個子句集，加入結(jié)論的否定以后進(jìn)行消解 第 4章 消解法 34 第 4章 消解法 解 ：先將問題謂詞表示如下： “任何通過計(jì)算機(jī)考試并獲獎的人都是快樂的” ?( )(x ),( c o m p u t e rxP a s s ))()),( xH a p p yp r i z exW i n ?? “任何肯學(xué)習(xí)或幸運(yùn)的人都可以通過所有考試” ?( ?)(x )()( xS t u d yy?)),()() yxP a s sxL u c k y ? “張不肯學(xué)習(xí)但他是幸運(yùn)的” ￢)( z h a n gS t u s y )( z h a n gL u c k y? “ 任何幸運(yùn)的人都能獲獎 ” ?( )(xL uck y)( x )),( p r i z exW i n? 結(jié)論“張是快樂的”的否定 ￢)( z h a n gHa p p y 35 第 4章 消解法 將上述謂詞公式轉(zhuǎn)化為子句集如下： (1) ￢ ?),( c o m p u t e rxP a ss ￢ )(),( xH a p p yp r i z exW i n ? (2) ￢ ),()( zyP a ssyS t u d y ? (3) ￢ ),()( vuP a ssuL u c k y ? (4) ￢ )( zh a n gS t u d y (5))( zh a n gLu c k y (6) ￢),()( p r i z ewW i nwLu c k y ? (7) ￢)( zh a n gH a p p y ( 本子句為結(jié)論的否定 ) 按謂詞邏輯的歸結(jié)原理對此子句進(jìn)行歸結(jié)，其歸結(jié)反演過程如 下 圖 所示。由于歸結(jié)出了子句，這就證明了張是快樂的。 36 第 4章 消解法 { w / x } { z h a n g / w } { z h a n g / u , c o m p u t e r / v } “快樂學(xué)生”問題的歸結(jié)反演樹 ￢?),( c o mp u t e rxP a s s￢)(),( xH a p p yp r i z exW i n ? )( z h a n gL u c k y ￢),()( vuP a s suL u c k y ? N I L ￢?),( c o m p u t e rz h a n gP a s s￢)( z h a n gL u c k y )( z h a n gL u c k y ￢),( c o m p u t e rz h a n gP a s s ￢)( z h a n gHa p p y ￢?),( c o mp u t e rwP a s s ?)( wHa p p y￢)( wL u c k y ),()( p r i z ewW i nwL u c k y ? ￢)( z h a n gL u c k y 消解策略 常用消解策略 支持集消解 有序消解策略 消解法舉例 第 4章 消解法 38 消解過程的計(jì)算復(fù)雜性 ? 定理證明的過程就是在子句集 S中不斷求消解式 ， 直到生成一個空子句 □ ? 現(xiàn)在涉及到求消解式的計(jì)算復(fù)雜性問題 ， 通常不考慮任何消解策略的盲目消解具有指數(shù)級的計(jì)算量：對于有 n個子句的子句集 ， 如果進(jìn)行 i次求消解式后得到空子句 ， 則計(jì)算復(fù)雜性是 O(n2i) ? 所以要研究加快消解速度 、 提高效率的各種消解策略 第 4章 消解法 39 常用消 解策略 ? 相關(guān)的消解策略主要包括： ? 刪除無用的子句 —永真式和隱含子句 ? 求隱含關(guān)系 —?dú)w類算法 ? 禁止無用子句產(chǎn)生 —限制參加消解的子句 / 限制被消解的文字 / 限制消解方式 ? 第 1種策略：支持集策略和動態(tài)支持集策略 ? 常用動態(tài)支持集策略 —線性消解 / 輸入消解 / 單元消解 ? 第 2種策略 —有序消解 第 4章 消解法 40 刪除策略 ? 刪除策略 —最直觀的一種策略就是刪除對消解沒有任何貢獻(xiàn)的子句 ， 減少進(jìn)行消解的子句數(shù)量 ， 從而提高效率 ? 刪除哪些子句 ？ 有 2類：永真式和隱含式 ? 第 1類是重言式 (永真式 )，