【文章內(nèi)容簡介】 名以保證每個(gè)量詞有其自己唯一的啞元。 47 (4) 消去存在量詞 用 Skolem函數(shù)代替存在的 x,就可以消去全部存在量詞，并寫成： (? y)P［ g(y),y］ 從一個(gè)公式消去一個(gè)存在量詞的一般規(guī)則是以一個(gè) Skolem函數(shù)代替每個(gè)出現(xiàn)的存在量詞的量化變量，而這個(gè) Skolem函數(shù)的變量就是由那些全稱量詞所約束的全稱量詞量化變量，這些全稱量詞的轄域包括要被消去的存在量詞的轄域在內(nèi)。 Skolem函數(shù)所使用的函數(shù)符號(hào)必須是新的，即不允許是公式中已經(jīng)出現(xiàn)過的函數(shù)符號(hào)。例如： (? y)(? x)P(x,y)被〔 (? y)P(g(y),y)〕代替，其中 g(y)為一 Skolem函數(shù)。 48 如果要消去的存在量詞不在任何一個(gè)全稱量詞的轄域內(nèi)，則用不含變量的 Skolem函數(shù)即常量。例如， (? x)P(x)化為 P(A)，其中常量符號(hào) A用來表示人們知道的存在實(shí)體。A必須是個(gè)新的常量符號(hào)，它未曾在公式中其它地方使用過。 49 (5) 化為前束形 把所有全稱量詞移到公式的左邊，并使每個(gè)量詞的轄域包括這個(gè)量詞后面公式的整個(gè)部分。所得公式稱為前束形。 (6) 把母式化為合取范式 任何母式都可寫成由一些謂詞公式和 (或 )謂詞公式的否定的析取的有限集組成的合取。這種母式叫做合取范式。 (7) 消去全稱量詞 消去明顯出現(xiàn)的全稱量詞。 50 提問：對(duì)于公式 (? z)(? y){(? x)P(x,y,z)∨( ? q)(?)(? e)Q(q,w,e,z)，在經(jīng)過消去存在量詞后，正確的公式為： A． (? y){P(B,y,A)∨( ? w)Q(C,w,D,A) B． (? y){P(B,y,A)∨( ? ? w)Q(C,w,g(w),A) , g(w)為一 Skolem函數(shù) C． (? y){P(g1(y),y,A)∨( ? w)Q(g２ (y),w,g３(w),A) 式中， (g1(y)， g２ (y)和 g３ (w)為 Skolem函數(shù) D． (? y){P(g1(y),y,A)∨( ? w)Q(g２ (y),w,g３(y,w),A) 式中， (g1(y)， g２ (y)和 g３ (y,w)為 Skolem函數(shù) 51 (8) 消去連詞符號(hào) ∧ 用｛ A， B｝代替 (A∧B) ，以消去明顯的符號(hào) ∧ 。反復(fù)代替的結(jié)果，最后得到一個(gè)有限集，其中每個(gè)公式是文字的析取。任一個(gè)只由文字的析取構(gòu)成的合適公式叫做一個(gè)子句。 (9) 更換變量名稱 可以更換變量符號(hào)的名稱，使一個(gè)變量符號(hào)不出現(xiàn)在一個(gè)以上的子句中。 52 例 將下列謂詞演算公式化為一個(gè)子句集 (? x)｛ P(x)→ ｛ (? y)［ P(y)→P(f(x,y)) ］ ∧ ～ (? y)［ Q(x,y)→P(y) ］｝｝ 53 說明 并不是所有問題的謂詞公式化為子句集都需要上述 9個(gè)步驟。對(duì)于某些問題，可能不需要其中的一些步驟。 54 消解推理規(guī)則 消解式 令 L1為任一原子公式， L2為另一原子公式； L1和 L2具有相同的謂詞符號(hào)，但一般具有不同的變量。已知兩子句 L1∨ α 和～L2∨ β ,如果 L1和 L2具有最一般合一者 σ ，那么通過消解可以從這兩個(gè)父輩子句推導(dǎo)出一個(gè)新子句 (α ∨ β )σ 。這個(gè)新子句叫做消解式。它是由取這兩個(gè)子句的析取，然后消去互補(bǔ)對(duì)而得到的。 55 消解式求法 (1) 假言推理 父輩子句 P ～ P∨Q( 即 P→Q) \ / \ / 消解式 Q 56 (2) 合并 (3) 重言式 (4) 空子句 (矛盾 ) ～ P P \ / \ / NIL (5) 鏈?zhǔn)?(三段論 ) 即取各子句的析取，然后消去互補(bǔ)對(duì)。 說明： 對(duì)合并、重言式、鏈?zhǔn)?(三段論 )請(qǐng)同學(xué)們自行閱讀。 57 含有變量的消解式 消解式求法 為了對(duì)含有變量的子句使用消解規(guī)則，必須找到一個(gè)置換，作用于父輩子句使其含有互補(bǔ)文字。 58 例子 P(x)∨ Q(x) Q［ f(y)］ 置換 σ =｛ f(y)/x｝ P［ f(y)］ 59 消解反演求解過程 基本思想 把要解決的問題作為一個(gè)要證明的命題，其目標(biāo)公式被否定并化成子句形，然后添加到命題公式集中去，把消解反演系統(tǒng)應(yīng)用于聯(lián)合集，并推導(dǎo)出一個(gè)空子句 (NIL)，產(chǎn)生一個(gè)矛盾，這說明目標(biāo)公式的否定式不成立，即有目標(biāo)公式成立，定理得證，問題得到解決，與數(shù)學(xué)中反證法的思想十分相似。 60 消解反演 反演求解的步驟 給出一個(gè)公式集 S和目標(biāo)公式 L，通過反證或反演來求證目標(biāo)公式 L，其證明步驟如下： (1)否定 L，得～ L； (2)把～ L添加到 S中去； (3)把新產(chǎn)生的集合｛～ L， S｝化成子句集； (4)應(yīng)用消解原理，力圖推導(dǎo)出一個(gè)表示矛盾的空子句 NIL。 61 ? 反演求解的正確性 設(shè)公式 L在邏輯上遵循公式集 S，那么按照定義滿足 S的每個(gè)解釋也滿足 L。決不會(huì)有滿足 S的解釋能夠滿足～ L的，所以不存在能夠滿足并集 S∪ ｛～ L｝的解釋。如果一個(gè)公式集不能被任一解釋所滿足，那么這個(gè)公式是不可滿足的。因此，如果 L在邏輯上遵循 S，那么 S∪ ｛～ L｝是不可滿足的?？梢宰C明，如果消解反演反復(fù)應(yīng)用到不可滿足的子句集，那么最終將要產(chǎn)生空子句 NIL。因此，如果 L在邏輯上遵循 S，那么由并集 S∪ ｛～ L｝消解得到的子句，最后將產(chǎn)生空子句；反之，可以證明，如果從 S∪ ｛～ L｝的子句消解得到空子句，那么 L在邏輯上遵循 S。 62 反演求解過程 步驟： (1)把由目標(biāo)公式的否定產(chǎn)生的每個(gè)子句添加到目標(biāo)公式否定之否定的子句中去。 (2)按照反演樹，執(zhí)行和以前相同的消解，直至在根部得到某個(gè)子句止。 (3)用根部的子句作為一個(gè)回答語句。 63 ? 分析： 答案求取涉及到把一棵根部有 NIL的反演樹變換為在根部帶有可用作答案的某個(gè)語句的一顆證明樹。由于變換關(guān)系涉及到把由目標(biāo)公式的否定產(chǎn)生的每個(gè)子句變換為一個(gè)重言式，所以被變換的證明樹就是一棵消解的證明樹，其在根部的語句在邏輯上遵循公理加上重言式，因而也單獨(dú)地遵循公理。因此被變換的證明樹本身就證明了求取辦法是正確的。 64 ? 例：儲(chǔ)蓄問題 前提：每個(gè)儲(chǔ)蓄錢的人都獲得利息。 結(jié)論：如果沒有利息，那么就沒有人去儲(chǔ)蓄錢 思考： 應(yīng)用消解反演求解如下問題： “如果無論約翰 (John)到哪里去，菲多(Fido)也就去那里，那么如果約翰在學(xué)校里，菲多在哪里呢 ?” 65 規(guī)則演繹系統(tǒng) 教學(xué)內(nèi)容：規(guī)則演繹系統(tǒng)屬于高級(jí)搜索推理技術(shù)，用于解決比較復(fù)雜的系統(tǒng)和問題。本節(jié)介紹規(guī)則演繹系統(tǒng)的定義及其三種推理方法：規(guī)則正向演繹系統(tǒng)、規(guī)則逆向演繹系統(tǒng)和規(guī)則雙向演繹系統(tǒng)。 教學(xué)重點(diǎn)：規(guī)則演繹系統(tǒng)的定義、正向推理和逆向推理過程。 教學(xué)難點(diǎn)：雙向演繹的匹配問題等。 教學(xué)方法：課堂教學(xué)為主。通過比較揭示正向推理、逆向推理和雙向推理的特點(diǎn)。 教學(xué)要求：掌握規(guī)則演繹系統(tǒng)的定義和正向推理、逆向推理的過程，了解規(guī)則雙向演繹系統(tǒng)。 66 ? 規(guī)則演繹系統(tǒng)的定義： 基于規(guī)則的問題求解系統(tǒng)運(yùn)用下述規(guī)則來建立： If→Then 其中， If部分可能由幾個(gè) if組成，而 Then部分可能由一個(gè)或一個(gè)以上的 then組成。 在所有基于規(guī)則系統(tǒng)中，每個(gè) if可能與某斷言 (assertion)集中的一個(gè)或多個(gè)斷言匹配。有時(shí)把該斷言集稱為工作內(nèi)存。在許多基于規(guī)則系統(tǒng)中， then部分用于規(guī)定放入工作內(nèi)存的新斷言。這種基于規(guī)則的系統(tǒng)叫做規(guī)則演繹系統(tǒng) (rule based deduction system)。在這種系統(tǒng)中，通常稱每個(gè) if部分為前項(xiàng) (antecedent)，稱每個(gè) then部分為后項(xiàng) (consequent)。 67 定義 正向規(guī)則演繹系統(tǒng)