【正文】 (~S?Q) ?(~T?Q) = {~S?Q, ~T?Q} 第四章 確定性推理 演繹推理 2/27/2023 35 命題邏輯消解反演的例子（續(xù)） 子句集： (1) P (2) ~P?~Q?R (3) ~S?Q (4) ~T?Q (5) T (6) ~R（目標求反） 歸結： (7) ~P?~Q (2, 6) (8) ~Q (1, 7) (9) ~T (4, 8) (10) nil (5, 9) 第四章 確定性推理 演繹推理 2/27/2023 36 謂詞邏輯消解反演的例子 ? 例： 已知： If Fido goes wherever John goes and if John is at school, where is Fido ? (?x)[AT(John, x) ? AT(Fido, x)] AT(John, School) 求證： (?x)AT(Fido, x) 子句集： ~AT(John, y) ? AT(Fido, y) AT(John, School) ~AT(Fido, x) ( ~(?x)AT(Fido, x) = (? x) ~AT(Fido, x) ) 第四章 確定性推理 演繹推理 2/27/2023 37 ~AT(Fido, x) ~AT(John, y) ?AT(Fido, y) 子句集： ~AT(John, y) ? AT(Fido, y) AT(John, School) ~AT(Fido, x) ~AT(John, x) {x/y} AT(John, School) nil {School/x} AT(Fido, School) 謂詞邏輯消解反演的例子（續(xù)） 第四章 確定性推理 演繹推理 2/27/2023 38 基于消解原理的問答系統(tǒng) ? 消解原理主要用來解決證明的問題，但有時我們希望得到如 x=?時， W(x)為真的回答 ? 消解原理是將結論的否定作為前提進行歸結，而為了回答問題，用由結論的否定構成的重言式作為前提進行歸結，得到的結論是問題的回答而不是空語句。 ? 歸結搜索策略一般包括：排序策略和限制策略 第四章 確定性推理 演繹推理 2/27/2023 44 排序策略 ? 歸結順序與狀態(tài)空間的擴展順序類似。 ? 寬度優(yōu)先： ? 先生成第 1層的所有歸結式．然后是第 2層所有的歸結式，依次類推，直到產生空子句或不能再進行歸結為止。 ? 線性輸入策略。 ? 刪除策略有幾種刪除方法： ? (1)純文字刪除法。 ? 因此，這樣的子句對歸結是無意義的，把它從子句集中刪去，不會影響子句集的不可滿足性。 ?重言式是真值為真的子句。 第四章 確定性推理 演繹推理 2/27/2023 50 支持集策略 ? 支持集策略： 每次歸結時．參與歸結的子句中至少應有一個是由目標公式的否定所得到的子句，或者是它們的后裔 ? 后裔的定義：設 α1是子句 ? α1 與另外某子句的歸結式是 α1 的后裔 ? α1 的后裔與其他子句的歸結式是 α1 的后裔。 ? 線性輸入策略是不完備的。 第四章 確定性推理 演繹推理 2/27/2023 53 消解方法小結 ? 求子句集，進行歸結，方法簡單 ? 通過修改證明樹的方法，提取回答 ? 方法通用 ? 求解效率低，不宜引入啟發(fā)信息 ? 不宜理解推理過程 第四章 確定性推理 演繹推理 2/27/2023 54 基于規(guī)則的演繹推理（一） ? 歸結反演系統(tǒng)解決問題的效率低下 ? 歸結演繹并非人類的自然思維方式，不利于人們從自然思維的角度組織問題的求解和提供問題求解所需的知識 ? 基于 規(guī)則的演繹推理，運用推理規(guī)則，直接推導目標公式 ? 這符合人的自然思維方式，也能通過規(guī)則 (作為啟發(fā)式知識 )更有效地引導演繹推理過程。 對于一個受存在量詞約束的變量，消去原則： ? 如果他不受全程量詞約束，則該變量用一個常量代替 ? 如果他受全程量詞約束，則該變量用一個函數代替，且全稱量詞變?yōu)榇嬖诹吭~。 第四章 確定性推理 規(guī)則的 演繹推理 —— 逆向演繹 2/27/2023 67 化目標表達式為與或形 ? 消去蘊涵符號： ～ P∨Q 取代 P→Q ? 減少否定符號的管轄域 ? 對變量標準化 ? 消去全稱量詞 ： 引入 Skolem函數 ? 消去存在量詞 第四章 確定性推理 規(guī)則的 演繹推理 —— 逆向演繹 2/27/2023 68 目標表達式化為與或形舉例 例： (?z) (?x)(?y){[(P(x) ?Q(x)) ?R(y)] ?U(z)} 前三步： 1, 消蘊涵符 2, 移動否定符 3, 變量標準化 等 3步與正向推理中化事實的表達式方法相同 4, 消全稱量詞 (skolem化 (對偶形 ) ） 原則：對于一個受全稱量詞約束的變量，如果他受存在量詞約束，則該變量用一個函數代替。當產生的圖包含有終止在目標節(jié)點上的一個解圖時，系統(tǒng)便成功地結束。 ? 事實是 有關問題狀態(tài)和環(huán)境的知識， ? 規(guī)則演繹的任務就是從給定的事實證明某個目標公式成立。 第四章 確定性推理 演繹推理 2/27/2023 52 祖先過濾策略 ? 祖先過濾策略 ：參與歸結的兩個子句中至少有一個是初始子句集中的子句，或者一個子句是另一個子句的祖先。即對一個不可滿足的子句集運用支持集策略進行歸結，最終總會導出空子句。 第四章 確定性推理 演繹推理 2/27/2023 49 包孕刪除法 ? 設 C1， C2是兩個子句，若存在置換 σ，使得C1σ? C2，則稱子句 C2包孕 C1 ? 例如， P(a)VQ(y)包孕 P(x) (σ={a/x}) ? P(a)VQ(y)包孕 Q(y) ? 對于一個子句集，刪去一個被別的子句包孕的子句，不會影響它的不可滿足性。 第四章 確定性推理 演繹推理 2/27/2023 48 重言式刪除法 ?如果一個子句中同時包含互補文字對，則稱該子句為重言式。 ? (3)包孕刪除法 第四章 確定性推理 演繹推理 2/27/2023 47 純文字刪除法 ? 如果某文字 L在子句集中不存在可與之互補的文字~L，則稱該文字為純文字。 第四章 確定性推理 演繹推理 2/27/2023 46 刪除策略 ? 如果在歸結時能把子句集中的無用子句刪除掉，這樣就會縮小尋找范圍，減少比較次數。 第四章 確定性推理 演繹推理 2/27/2023 45 限制策略 ? 限制策略不涉及被歸結子句的排序．只允許某些歸結發(fā)生。 ? 把原始子句看成 0層歸結式。 ? 下面以猴子摘香蕉問題為例來說明 第四章 確定性推理 演繹推理 2/27/2023 39 用消解原理解猴子摘香蕉問題 ? 為了把狀態(tài)空間的算符描述與謂詞演算結合起來，將狀態(tài)添到謂詞上； ? 將算符看成是把一種狀態(tài)映射成另一種狀態(tài)的函數； ?