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