【正文】 ○ ○ P ∨﹁ Q ﹁ Q ○ ○ Q ∨﹁ R ﹁ R ○ ○ R □ ○77 單元消解 ? [單元消解定義 ]在動態(tài)支持集消解定義中令Sn2={Sn 中所有單子句和單因子 }，則此策略稱為單元消解策略 (也叫單項消解 ) / 這樣，每次參加消解的一方總有一個是單項 ? 例 4： S={P∨ Q,﹁ P∨ R,﹁ Q∨ R,﹁ R}， 其消解過程如圖所示 。 Cn稱為消解時的中心子句，另一方稱為邊子句 ? 線性消解是完備的 第 4章 消解法 75 線性消解 ? 注意：在現(xiàn)行消解過程中 ， 初始中心句的選取很重要 ， 不能任意選擇 。其消解過程可由下圖說明 第 4章 消解法 S ’ S ’ ○﹁ P ∨ Q ○﹁ P ∨﹁ Q ○ P ∨﹁ Q ○﹁ P ∨﹁ Q ○ ﹁ P ○﹁ Q ○ P ∨ Q ○ Q ○ □73 動態(tài)支持集消解 ? 判斷 S―S’ 是否可滿足，需要花費時間，所以要尋找更好的策略。 ? 主要介紹第 1種策略 ， 即對每次參加消解的子句作出規(guī)定 第 4章 消解法 70 支持集消解 ? 一般來說 ， 消解法常常用來證明C1∧C 2∧ … ∧C n∧ ﹁ C不可滿足 ， 此即C1∧C 2∧ … ∧C n→C ? 因為前提子句集合 {Ci}應該是可滿足的 ， 所以消解不應在各個 Ci間進行 ，而應在 Ci和 ﹁ C之間或 ﹁ C內部進行 ? 支持集策略：推廣此想法，限定消解雙方不能都取自子句集的某個子集 第 4章 消解法 71 支持集消解 (2) ? [定義 ]支持集消解：設 S為子句集 ， S’為其子集 ， 若 S―S’ 是可滿足的 ， 則稱 S’是 S的一個支持集 。 第 4章 消解法 67 歸類算法 (3) ? 注意： Uk+1=Φ表明 Uk和 W中已不存在可消解的子句 ， 所以沒有 R(C1, C2)， 其中 C1∈ Uk, C2∈ W ? 算法工作前 ， 讓 D中變量均以常量置換 ， 是隱含關系定義所要求的：因為根據(jù)定義 ， 置換 ?只能對 C實行 ， 當算法進行中又要作消解 ， 即 D的部分 (W中文字 )要作消解 ， 則必然要作置換 ， 所以只能先把 D中變量全部置換為常量后才能阻止消解中對 D的置換 第 4章 消解法 68 歸類算法舉例 ? 例子： C=﹁ P(x)∨ Q(f(x), a) D=﹁ P(h(y))∨ Q(f(h(y)), a)∨ P(z) ? 首先作 ?={b/y, c/z}，則 W={P(h(b)),﹁Q(f(h(b)), a),﹁ P(c)}={W1, W2, W3} (1)U0={C}={﹁ P(x)∨ Q(f(x), a)} (2)U0不包含 □ ， 則 U1={R(C, W)}={Q(f(h(b)), a), ﹁P(h(b))}， 其中 Q(*)是 U0與 W1的消解式 ， ﹁ P(*)是U0與 W2的消解式 ， U1不空繼續(xù) (3)U2顯然包含 □ ， 因為 Q(f(h(b)), a)∈ U1而 ﹁ Q(f(h(b)), a)∈ W 可消解為 □ ， 同樣 ﹁ P(h(b))∈ U1 而P(h(b))∈ W可消解為 □ 。 通常不考慮任何消解策略的盲目消解具有指數(shù)級的計算量：對于有 n個子句的子句集 ， 如果進行 i次求消解式后得到空子句 ， 則計算復雜性是 O(n2i) ? 所以要研究加快消解速度 、 提高效率的各種消解策略 第 4章 消解法 62 常用消 解策略 ? 本節(jié)介紹相關的消解策略，主要內容包括： ? 刪除無用的子句 — 永真式和隱含子句 ? 求隱含關系 — 歸類算法 ? 禁止無用子句產(chǎn)生 — 限制參加消解的子句 / 限制被消解的文字 / 限制消解方式 ? 第 1種策略：支持集策略和動態(tài)支持集策略 ? 常用動態(tài)支持集策略 — 線性消解 / 輸入消解 / 單元消解 ? 第 2種策略 — 有序消解 ? 消解法例子 第 4章 消解法 63 刪除策略 ? 最直觀的一種策略就是刪除對消解沒有任何貢獻的子句 ， 減少進行消解的子句數(shù)量 ， 從而提高效率 。 Q Q 172。P∨ 172。從而使新否節(jié)點下面的語義樹分支無必要存在，即引起語義樹的倒塌 第 4章 消解法 56 消解法的完備性 (2) ? 重復上述語義樹的倒塌過程，直到語義樹僅由樹根組成為止。 ? [推論 ]若 S是可滿足的，則 S推導出的任一子句也是可滿足的，即不能推出空子句。 這是因為取因子之后 ， 子句 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?所余部分。 故 W的 mgu不存在 。合一置換也叫通代 ? [定義 ]最一般合一置換 (最廣通代 )：如果 ? 和 ?都是公式組 {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。經(jīng)過 DavisPutnam預處理以后的子句集與原子句集在不可滿足性上等價 第 4章 消解法 38 消解法 置換與合一 消解式 消解法的實施 第 4章 消解法 39 消解法的形式 ? 進一步推廣 DavisPutnam規(guī)則 ， 就得到了消解法 。 T’存在 有限路徑和末端否節(jié)點，即使 S的某個子句的某基例為假。 ? [必要性 ]已知 S存在有限的封閉語義樹 T。 這樣實際上構成的是一個有限樹 ? 所以就有 Herbrand定理：子 句集 S不可滿足 ， 當且僅當它所對應的每棵完備語義樹均包含一個有限的封閉子樹 (封閉語義樹 ) 第 4章 消解法 31 Herbrand定理 ? Herbrand定理有兩種形式 ? Herbrand定理 I：子句集 S不可滿足，當且僅當它所對應的每棵完備語義樹均包含一個有限的封閉子樹 (封閉語義樹 ) ? 證明： ? [充分性 ]設 S是不可滿足的， T是 S的一株完備語義樹。這是一種很直觀的研究方式，稱為語義樹方法 ? 設 S={P, Q, R}，則 H∞={a}， ~H={P(a), Q(a), R(a)} (只有一個常量 a，在語義樹中可省略 ) ? 因為是二值邏輯，研究每個基原子 (即 S的原子公式 )的取值可以通過原子及其否定 (即文字 )來觀察 / 構造如下二叉形式的語義樹 第 4章 消解法 21 語義樹示例 ? 通常用 I(Ni)表示從根節(jié)點到節(jié)點 Ni分枝上所標記的所有文字的并集 。 ? Skolem標準形：在前束范式中消去存在量詞后得到的公式 第 4章 消解法 10 消去存在量詞 ? 消去存在量詞的步驟： (1)若存在量詞不在任何全稱量詞之后 ， 則公式中被存在量詞量化的變量以某個不同于公式中任何其他常量名字的常量 c代替 ， 并消去存在量詞； (2)若存在量詞在 k個全稱量詞之后 ， 則公式中被存在量詞量化的變量用被前 k個全稱量詞量化的變量 x1～ xk的某個函數(shù) f(x1～ xk)的形式代替 ，f的名字不同于公式中任何其他函數(shù)的名字 ，但對函數(shù)形式?jīng)]有要求；然后消去存在量詞 / 函數(shù) f稱為 Skolem函數(shù) 第 4章 消解法 11 公式轉化為子句集的步驟 (1) ? 公式 A化為子句集 S， 其實現(xiàn)步驟共 9步 ，如下： (1)消去等價和蘊含符號：蘊含轉化為析取 (2)將否定符號轉移到每個謂詞之前：應用狄摩根定律 (3)變量標準化：約束變量各不相同 (4)消去存在量詞：存在量詞不受全稱量詞約束，則變量用常量替換 /如果存在量詞受全稱量詞約束，則使用 Skolem函數(shù)替換相應變量 —— 得到 Skolem標準形 第 4章 消解法 12 公式轉化為子句集的步驟 (2) (5)公式化為前束型：全部全稱量詞移到公式的最前面 /得到的兩部分稱為前綴和母式 (6)母式化為合取范式：外層連接符全部是合取 ， 里層連接符全部為析取 (7)去掉所有全稱量詞 (8)母式化為子句集：每個合取項間的合取符號 (∧ )用逗號代替 ， 即得子句集 (9)子句變量標準化：每個子句中的變量各不相同 第 4章 消解法