【正文】 解釋已經(jīng)使 S的某個子句為假 ， 因此再擴充路徑仍然只能使同一子句為假 ， 所以沒有擴充 、 延伸的必要 □ 第 4章 消解法 72 有限封閉語義樹 ? 上例說明 ， 從不可滿足的角度來說 ， 對于無限完備語義樹只需搜索到一個否節(jié)點 ，則該分枝即被證明為不可滿足 。 這樣實際上構(gòu)成的是一個有限樹 ? 所以就有 Herbrand定理： 子 句集 S不可滿足 ， 當且僅當它所對應的每棵完備語義樹均包含一個有限的封閉子樹 (封閉語義樹 ) 第 4章 消解法 73 作業(yè) ? 1. 將合式公式化為子句型 ? 2. 求出下列子句集的最一般合一（ mgu） ? 3 “有些患者喜歡任一醫(yī)生，沒有任一患者喜歡任一庸醫(yī)，所以沒有庸醫(yī) ” 用消解法證明上述結(jié)論 [ ( ) [ [ ( ) ( ( , ) ) ] [ ( , ) ( ) ] ] ]x P x y p y P f x y y Q x y P y? ? ? ? ? ? ? ?{ ( , , ( ( ) ) , ( , ( ) , ( ) ) }W P a x f g y P z f z f u?74 參考書目 ? Stuart Russell / Peter Norvig: AIMA 第 7章 / 第 9章 ? 陸汝鈐 編著 : 人工智能 (下冊 ) 第 17章 ? 石純一、黃昌寧、王家 [廣欽 ]，人工智能原理，清華大學出版社， 1993年 10月第 1版 ? 田盛豐、黃厚寬，人工智能與知識工程，中國鐵道出版社， 1999年 8月第 1版 ,第 5章 第 4章 消解法 75 附錄 76 子句的推導 ? 子句的推導定義： ? 給定子句集 S， 如果存在一個有限的子句序列 C1,C2,… ,Ck， 使得每個 Ci或者屬于 S，或者是 C1～Ci1的某些子句的消解式 ， 且 Ck=C， 則從 S可以推導出子句 C， 稱此子句序列為 C的推導 。 當 C為空子句 □ 時 ， 也稱該序列為 S的一個否證 。 第 4章 消解法 77 Herbrand定理證明 ? Herbrand定理有兩種形式 ? Herbrand定理 I：子句集 S不可滿足，當且僅當它所對應的每棵完備語義樹均包含一個有限的封閉子樹 (封閉語義樹 ) ? 證明： ? [充分性 ]設 S是不可滿足的， T是 S的一株完備語義樹。設 B是 T的任意一個分支路徑，則 IB是對應該分支上 S的一個解釋 由 S的不可滿足性知 IB使 S的某子句的某個基例為假。則 B上有節(jié)點 N且 N是 T的否節(jié)點 第 4章 消解法 78 Herbrand定理 I的證明 因為 S中子句的個數(shù)有限，每個子句所含的文字也有限，則 IB中的文字個數(shù)也有限，因此否節(jié)點 N離 T的根節(jié)點只有有限步。 因為 T是二叉樹且每個節(jié)點只有兩個子節(jié)點，由 B的任意性可知， T所有分支上的否節(jié)點所構(gòu)成的封閉語義樹必是有限的。 ? [必要性 ]已知 S存在有限的封閉語義樹 T。設 I是S的任一解釋，則其落在 T的某個分支 B上， B上必有否節(jié)點 N存在 可知 I(N)使 S的某子句的某個基例 C’為假。由 I(N)?I及任意性，可知 S是不可滿足的 ★ 第 4章 消解法 79 Herbrand定理 II(1) ? Herbrand定理 II： S是不可滿足的，當且僅當存在 S的一個不可滿足的有限基例集 ? 證明： ? [充分性 ]設 S是不可滿足的，及 T是 S的一個完備語義樹。由 Herbrand定理 I知存在 T的有限封閉子樹 T’。 T’存在 有限路徑和末端否節(jié)點，即使 S的某個子句的某基例為假。 將基例加起來，即得一 個不可滿足的有限基例集 第 4章 消解法 80 Herbrand定理 II(2) ? [必要性 ]設 S’?S且不可滿足的有限基例集。設 I是 S的任一解釋，應有 S’的解釋 I’?I，已知 I’使 S’的某個基例為假，于是 I使其為假，即使 S為假，故 S不可滿足 ★ ? 如同語義樹的結(jié)構(gòu)不唯一，不可滿足的有限基子句集也不唯一 ? 從自動證明的角度，定理 II是基礎 第 6章 消解法 81 不可滿足基子句集 ? 不可滿足基子句集的生成：可通過逐步測試基子句集中各有限子集的方法來找出，此為 Gilmore算法 (算法略，參見陸著 ) / 當 S不可滿足時，該算法一定結(jié)束 (半可判定 ) ? 但該算法具有指數(shù)復雜性，為此提出了改進規(guī)則，改進的規(guī)則稱為 DavisPutnam預處理 第 4章 消解法 82 DavisPutnam預處理 (1) ? DavisPutnam預處理： (1)重言式 (永真式 )刪除規(guī)則：刪去所有重言式子句 ， 因為與不可滿足性無關(guān)； (2)單文字 (單句節(jié) )刪除規(guī)則：如果 S中包含一個單文字子句 L(即只有一個原子公式 )， 則從 S中刪去所有含 L的子句 ， 從 S中刪去所有子句中的 ﹁ L文字 。 經(jīng)過如此處理的子句集為 S’， 若 S’為空 ， 則 S是可滿足的 ， 若 S’非空 ， 則 S’與 S同是不可滿足的； (3)純文字刪除規(guī)則：如果 S中只包含文字 L而不包含 ﹁ L， 則刪去所有包含 L的子句； 第 4章 消解法 83 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章 消解法 84 消解法的合理性 ? [合理性定理 ]若從子句集 S可以推導出子句 C，則 C是 S的邏輯推論 (或 S邏輯蘊含 C)。 ? [推論 ]若 S是可滿足的，則 S推導出的任一子句也是可滿足的，即不能推出空子句。 ? 其逆否形式：若 S推導出空子句□，則 S是不可滿足的。 ? 此為消解原理的合理性定理。即只要找出一個推出空子句的過程，則 S就不可滿足 第 4章 消解法 85 消解法的完備性 (1) ? 消解法是完備的 —即如果公式 X是子句集 S的邏輯推論，則 X可以從 S中推出 ? [完備性定理 ]子句集 S是不可滿足的，當且僅當從 S可推導出空子句□ ? 消解過程與語義樹倒塌之間的聯(lián)系： ? 從 S的語義樹 T出發(fā)，必有兩個否節(jié)點所對應的子句可作歸結(jié)，將歸結(jié)式放入 S，則否節(jié)點的位置提升，即原來兩個否節(jié)點的父節(jié)點成為否節(jié)點。從而使新否節(jié)點下面的語義樹分支無必要存在，即引起語義樹的倒塌 第 4章 消解法 86 消解法的完備性 (2) ? 重復上述語義樹的倒塌過程，直到語義樹僅由樹根組成為止。此時樹根是否節(jié)點，則 I(N0)= ?，即已歸結(jié)為空子句 □。 ? 舉例如下： S={P, 172。P∨ Q, 172。P∨ 172。Q} 第 4章 消解法 T N 0 T * N 0 T *1 N 0 P 172。 P P 172。 P N 11 N 12 N 11 N 12 N 11 N 12 Q 172。 Q Q 172。 Q N 21 N 22 N 23 N 24 N 21 N 2287 提升引理 ? 歸結(jié)過程與語義樹的倒塌過程是一致的 ? 進一步推廣：由基例間 (語義樹對應的形式 )可作歸結(jié)，到實現(xiàn)子句間可作歸結(jié)：即常量子句到變量子句的歸結(jié) / 于是得到提升引理 ? [提升引理 ]若 C1’和 C2’分別是子句 C1和 C2的例子句， C’是 C1’和 C2’的歸結(jié)式，則存在 C1和 C2的一個歸結(jié)式 C，使得 C’是 C的例子句 第 4章 消解法 88 消解法完備性定理 (1) ? 簡述完備性定理的證明過程： ? 必要性：存在 S到□的歸結(jié)過程，□是 S的邏輯推論，由合理性定理知 S是不可滿足的 ? 充分性： S不可滿足，由 Herbrand定理知存在有限封閉語義樹，必有二叉樹中 2個兄弟節(jié)點均為否節(jié)點，即使某 2個 S的基例為假 該 2個基例必可作歸結(jié) (有互補原子 )，則歸結(jié)式使其父節(jié)點成為否節(jié)點 (使歸結(jié)式為假 ) 第 4章 消解法 89 消解法完備性定理 (2) ? 將歸結(jié)式并入 S，則該父節(jié)點是并集的否節(jié)點，因此引起語義樹的倒塌 ? 重復上述過程至語義樹倒塌為只剩根節(jié)點且為否節(jié)點，說明 S∪ {R’,...}有限集必包含□。即存在 S到□的基例歸結(jié)過程 ? 由提升引理知必存在 S到□的子句歸結(jié)過程 ★ ? 關(guān)于消解法完備性的一個證明 (Robinson)見教材 p230~231 第 4章 消解法 90 消解法正確性的證明過程 存在 S消解為空的過程 ??存在有限封閉語義樹 (倒塌 ) ??Herbrand解釋不可滿足 ??子句集 S不可滿足 ??公式 G=A∧ ﹁ B(﹁ (A→B)) [子句集合 ]是不可滿足的 ??A→B 是有效的 第 4章 消解法 ?定理 S ?Herbrand定理 ?完備性定理 ?反證法