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