【正文】 人工智能原理 第 4章 消解法 本章內(nèi)容 消解法的基本思想 消解法 消解策略 Herbrand定理 參考書目 第 4章 消解法 消解法的基本思想 第 4章 消解法 4 消解法的基本思想 ? 從第 3章邏輯系統(tǒng)中可知 ， 邏輯推理必須考慮其有效性 (即 ∑|=A)， 即對(duì)論域中的任何賦值都能保證公式為真 ? 從有效性和可滿足性的關(guān)系可知 ， 有效性等價(jià)于其否命題的不可滿足性 ? 證明一個(gè)邏輯公式的有效性就是證明其公式的非的不可滿足性 (恒為假 ) ? 這樣就引出了消解法 ， 其基本思想就是反證法 第 4章 消解法 5 消解法基本思想 :反證法 ? 即：要證命題 (理解為經(jīng)典邏輯的公式 )A恒為真 ， 等價(jià)于證 ﹁ A恒為假 ? 從語義上解釋 ， 恒為假就是不存在一個(gè)論域上的一個(gè)賦值 (可稱為解釋 )， 使 ﹁ A為真 ， 即對(duì)所有的論域上的所有賦值 ，﹁ A均為假 ? 但是 ， 論域本身和解釋有無窮多個(gè) ， 不可能一一驗(yàn)證 第 4章 消解法 6 基本思想 (1) ? Herbrand提出：從所有解釋當(dāng)中選出一種有代表性的解釋 ， 并嚴(yán)格證明一旦命題在代表性解釋中為假 ， 則在所有解釋中為假 ? Herbrand定義了這樣的論域和代表性解釋，稱為 Herbrand論域 (H論域 )和 Herbrand解釋 (H解釋 ) ? 后面會(huì)看到：公式 A(無 ?前束范式 )是不可滿足的，當(dāng)且僅當(dāng) A(通過子句集 )在所有 Herbrand賦值下都取假值 第 4章 消解法 7 基本思想 (2) ? 這樣，在證假 (不可滿足 )的意義上使公式與子句集的語義解釋等價(jià)、 并與 H解釋等價(jià)，作為消解法的開端 ? 引入語義樹 ， 讓所有解釋都展現(xiàn)在語義樹上 ， 以便 找到 H解釋 。 ? 最后在改進(jìn)尋找解釋算法的復(fù)雜性中發(fā)現(xiàn)了消解式 ， 從而構(gòu)成了消解法的完整理論基礎(chǔ) ? 消解也叫歸結(jié)，本章混用這兩個(gè)稱呼 第 4章 消解法 消解法 公式到子句集的轉(zhuǎn)換 合一算法 消解式 消解法的實(shí)施 第 4章 消解法 9 消解法的形式 ? 消解法舉例： ? 此時(shí)只要使用單文字刪除規(guī)則就可以推出結(jié)論 Q。 但是如果子句中包含變量 ， 則常常必須經(jīng)過變量置換才能進(jìn)行消解 第 4章 消解法 ??????? )( QPQPPS10 歸結(jié)規(guī)則 ? 歸結(jié) —兩個(gè)互補(bǔ)文字消去 ? 單元?dú)w結(jié)規(guī)則 —一個(gè)子句和一個(gè)文字進(jìn)行互補(bǔ)文字消去 ? 全歸結(jié)規(guī)則 —兩個(gè)子句中消去互補(bǔ)文字 11 1 1..... . .. .kii i kl l m mll l l l???? ??? ? ? ? ?第 4章 消解法 111 1 1 1 1 1. . . . . .. . . . . . . . . . . .kniji i k j j nl l m m lml l l l m m m m? ? ? ?? ? ? ? ??? ? ? ? ? ? ? ? ? ? ?11 公式與子句集的等價(jià) ? 有定理 S：給定公式 A及相應(yīng)的子句集 S，則 A是不可滿足的當(dāng)且僅當(dāng) S是不可滿足的 ? 實(shí)現(xiàn)消解法的基礎(chǔ)是把參與推理的每個(gè)公式都轉(zhuǎn)化為子句集 / 通過逐步對(duì)消子句集合中互補(bǔ)的文字 (即 L和 ﹁ L)而最終得到一個(gè)空子句 □ ， 證明原來的公式是不可滿足的 第 4章 消解法 12 消解法證明的步驟 ? 證明一個(gè)公式 A在給定論域下恒為真 ， 也就是要證明 ﹁ A恒為假 ? 將 ﹁ A轉(zhuǎn)化為一個(gè)子句集 ， 集合中元素為原子公式或其析取 / 通過其中正負(fù)原子公式的合并 (此時(shí)恒為真 ， 對(duì)證假不起作用 ， 因此消去 ) / 最后集合為空 ， 說明是不可滿足的 ，即恒為假 ? 通常形式：證明 ﹁ (A→ B)為假即 A∧ ﹁ B為假 ， 也即對(duì)應(yīng)子句集歸結(jié)為空子句 第 4章 消解法 13 消解法證明的步驟 1. 寫出謂詞關(guān)系公式 2. 用反演法寫出謂詞表達(dá)式 3. SKOLEM標(biāo)準(zhǔn)型 4. 子句集 S 5. 對(duì) S中可消解的字句進(jìn)行消解（先進(jìn)行合一置換） 6. 消解式仍放入 S中，反復(fù)消解過程 7. 得到空字句 8. 得證 14 公式到子句集的轉(zhuǎn)換 ? 首先復(fù)習(xí)幾個(gè)定義： ? 文字 (literal)：正原子公式和負(fù)原子公式稱為文字 ， 同一原子公式的正和負(fù)稱為互補(bǔ)的 ? 子句 (clause)：文字的析取稱為子句 ? 合取范式：形如 A1∧ A2∧ … ∧ An的公式 ， 其中 A1～ An均為子句 ? 前束范式：形如 (Q1x1… Qn xn)M(x1… xn)的公式 ， M中不再含有量詞 ， Q是量詞 ? Skolem標(biāo)準(zhǔn)形：在前束范式中消去存在量詞后得到的公式 第 4章 消解法 15 消去存在量詞 ? 消去存在量詞的步驟： (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章 消解法 16 公式轉(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)公式化為前束型：全部存在量詞和全稱量詞移到公式的最前面 /得到的兩部分稱為前綴和母式 第 4章 消解法 17 公式轉(zhuǎn)化為子句集的步驟 (2) (5)消去存在量詞：存在量詞不受全稱量詞約束 ，則變量用常量替換 /如果存在量詞受全稱量詞約束 ， 則使用 Skolem函數(shù)替換相應(yīng)變量 ——得到 Skolem標(biāo)準(zhǔn)形 (6)母式化為合取范式：外層連接符全部是合取 ，里層連接符全部為析取 (7)去掉所有全稱量詞 (8)母式化為子句集：每個(gè)合取項(xiàng)間的合取符號(hào) (∧ )用逗號(hào)代替 ， 即得子句集 (9)子句變量標(biāo)準(zhǔn)化：每個(gè)子句中的變量各不相同 第 4章 消解法 18 合一算法 ? [定義 ]置換 (或代換 )：設(shè) x1～ xn是 n個(gè)變量，且各不相同， t1～ tn是 n個(gè)項(xiàng) (常量、變量、函數(shù) )， ti≠xi，則有限序列 {t1/x1, t2/x2 …t n/xn}稱為一個(gè)置換 ? 置換可以作用于謂詞公式，也可以作用于項(xiàng)。置換 θ={t1/x1, t2/x2 …t n/xn}作用于謂詞公式 E就是將 E中變量 xi均以 ti代替，其結(jié)果用 E?表示 / 作用于項(xiàng)的含義相同 第 4章 消解法 19 關(guān)于置換 ? 例： ?={a/x, f(b)/y, u/z} E=P(x, y, z) t=g(x, y) E?=P(a, f(b), u) t?=g(a, f(b)) ? [定義 ]置換乘積 (合成 )：設(shè) ?和 ?是 2個(gè)置換 ， 則先 ?后 ?作用于公式或項(xiàng) ， 稱為置換乘積 ， 用 ???表示 (E???) ? 一般來說 ， 置換乘積的結(jié)合律成立 ，即 (???)??=??(???)， 但交換律不成立 第 4章 消解法 20 合一置換 ? [定義 ]合一置換：設(shè)有一組謂詞公式 {E1～Ek}和置換 ?，使 E1?=E2?=…=E k?， 則 ?稱為合一置換， E1～ Ek稱為可合一的。合一置換也叫通代 ? [定義 ]最一般合一置換 (最廣通代 )：如果 ? 和 ?都是公式組 {E1～ Ek}的合一置換，且有置換 ?存在，使得 ?=???，則 ?稱為公式組{E1～ Ek}的最一般合一置換，記為 mgu (most general unification) 第 4章 消解法 21 分歧集 ? 在介紹 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。 ? 分歧集性質(zhì)：分歧集的出現(xiàn)處一定是謂詞或項(xiàng)的開始處 / 求最廣合一置換只考察項(xiàng)的分歧 第 4章 消解法 22 mgu求解算法 ? 求 mgu算法 (合一算法 ) ? 設(shè) W是謂詞組 ， ? 表示空置換 (即置換序列為空 )， 則算法如下： (1)k=0， W0=W， ?0=?； (2)如果 Wk中各謂詞完全一樣 ， 則算法結(jié)束 ， ?k是 W的mgu， 否則求 Wk的分歧集 Dk； (3)若 Dk含變量 xk以及項(xiàng) tk的首符號(hào)且 xk在 tk中不出現(xiàn) ，則繼續(xù)執(zhí)行算法 ， 否則 W的 mgu不存在 ， 算法停止； (4)令 ?k+1=?k?{t k/x k}， Wk+1= Wk{t k/x k}； (5)k=k+1， 轉(zhuǎn) (2) 第 6章 消解法 23 mgu存在條件 ? mgu存在的條件：如果有限謂詞組 W是可合一的，則上述算法一定成功結(jié)束并給出其存在 ? 求 mgu的預(yù)置條件：應(yīng)把所有謂詞中的變量換成不同名字的變量 。 (不過 ，