【正文】 x) ? R(f(x))?U(a)] ? [~Q(x))? R(f(x))?U(a)]} 7, 隱去全程量詞 {[~P(x) ? R(f(x))?U(a)] ?[~Q(x))? R(f(x))?U(a)]} 第三章 一般搜索原理 消解原理 2/27/2023 78 化子句集例 （續(xù) 3） 8, 表示為子句集 {~P(x) ? R(f(x))?U(a), ~Q(x))? R(f(x))?U(a)} 9, 變量標準化（變量換名） {~P(x1) ? R(f(x1))?U(a), ~Q(x2))? R(f(x2))?U(a)} 第三章 一般搜索原理 消解原理 2/27/2023 79 消解推理規(guī)則 ? L L2為任一原子公式，他們具有相同的謂詞符號，但一般變量名不同 ? 已知兩子句 L1∨ α和 ～ L2∨ β ? 如果 L L2具有最一般合一者 σ ? 那么可得新子句 (α∨ β) σ ? 這個 新子句叫做消解式 第三章 一般搜索原理 消解原理 2/27/2023 80 命題邏輯的消解推理舉例 第三章 一般搜索原理 消解原理 假言推理： P ～ P∨Q (P→Q ） 消解式 ： Q 合并： P∨Q ～ P∨Q 消解式 ： Q∨Q = Q 重言式： P ∨Q ～ P∨ ～ Q 消解式 ： P∨ ～ P 或 Q∨ ～ Q 空子句： P ～ P 消解式 ： NIL 三段論： ～ P∨Q (P→Q ） ～ Q∨R (Q→R ） 消解式 ：～ P∨R (P→Q ） 2/27/2023 81 謂詞邏輯的消解推理舉例 第三章 一般搜索原理 消解原理 B(x) ～ B(x)∨C(x ） 消解式 ： C(x) P(x)∨Q(x ） ～ Q[f(y)] 消解式 ： P[f(y)] 置換 ： f(y)/x P[x,f(y)]∨Q(x)∨R[f(a),y] ～ P[f(f(a)),z]∨R(z,w ） 消解式 ： Q[f(f(a))]∨R[f(a),y]∨R[f(y),w] 置換 ： f(f(a))/x, f(y)/z 2/27/2023 82 消解反演求解過程 ? 消解反演 是利用 消解原理進行命題證明。 ? 給定公式集 S和目標公式 L ? 證明 公式 L的步驟如下： ?否定 L ，得～ L ?把～ L 添加到 S中去 ?把新產(chǎn)生的集合 {～ L ,S}化成子句集 ?應(yīng)用消解原理力圖推導(dǎo)出一個表示矛盾的空子句 第三章 一般搜索原理 消解原理 2/27/2023 83 命題邏輯消解反演的例子 設(shè)公理集： P, (P?Q) ?R, (S?T) ?Q, T 求證： R 子句集： (1) P (2) ~P?~Q?R (3) ~S?Q (4) ~T?Q (5) T (6) ~R（目標求反） 化子句集： (P?Q) ?R = ~(P?Q)?R = ~P?~Q?R (S?T) ?Q = ~ (S?T)?Q = (~S?~T)?Q = (~S?Q) ?(~T?Q) = {~S?Q, ~T?Q} 第三章 一般搜索原理 消解原理 2/27/2023 84 命題邏輯消解反演的例子（續(xù)） 子句集： (1) P (2) ~P?~Q?R (3) ~S?Q (4) ~T?Q (5) T (6) ~R（目標求反） 歸結(jié)： (7) ~P?~Q (2, 6) (8) ~Q (1, 7) (9) ~T (4, 8) (10) nil (5, 9) 第三章 一般搜索原理 消解原理 2/27/2023 85 謂詞邏輯消解反演的例子 ? 例： 已知： 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 86 ~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 87 基于消解原理的問答系統(tǒng) ? 消解原理主要用來解決證明的問題，但有時我們希望得到如 x=?時， W(x)為真的回答 ? 消解原理是將結(jié)論的否定作為前提進行歸約，而為了回答問題，用由結(jié)論的否定構(gòu)成的重言式作為前提進行歸約，得到的結(jié)論是問題的回答而不是空語句。這個過程稱為修改證明過程（或修改歸約過程）。 ? 下面以猴子摘香蕉問題為例來說明 第三章 一般搜索原理 消解原理 2/27/2023 88 用消解原理解猴子摘香蕉問題 ? 為了把狀態(tài)空間的算符描述與謂詞演算結(jié)合起來，將狀態(tài)添到謂詞上； ? 將算符看成是把一種狀態(tài)映射成另一種狀態(tài)的函數(shù)； ? 問題簡化成沒有 goto()規(guī)則； 第三章 一般搜索原理 消解原理 c 2/27/2023 89 猴子摘香蕉問題的表示 問題可以描述如下 ： 1, ~ONBOX(s0) 2, (?x)(?s)(~ONBOX(s) ? AT(box, x, push(x, s))) 3, (?s)(ONBOX(climbbox(s))) 4, (?s)((ONBOX(s) ? AT(box, c, s)) ? HB(grasp(s))) 5, (?x)(?s)(AT(box, x, s) ? AT(box, x, climb(s))) 求解： (?s)HB(s) 第三章 一般搜索原理 消解原理 2/27/2023 90 猴子摘香蕉問題的子句集 1, ~ON(s0) 2, ON(s1) ? AT(box, x1, push(x1, s1)) 3, ON(climb(s2)) 4, ~ON(s3) ? ~AT(box, c, s3) ? HB(grasp(s3)) 5, ~AT(box, x4, s4) ?AT(box, x4, climb(s4)) 6, ~HB(s5) 第三章 一般搜索原理 消解原理 2/27/2023 91 ~HB(s5) ~ON(s3) ? ~AT(box, c, s3) ? HB(grasp(s3)) ~ON(s3) ? ~AT(box, c, s3) {grasp(s3)/s5} ON(climb(s2)) {climb(s2)/s3} ~AT(box, c, climb(s2)) ~ON(s0) ON(s1) ? AT(box, x1, push(x1, s1)) {s0/s1} AT(box, x1, push(x1, s0)) ~AT(box, x4, s4) ?AT(box, x4, climb(s4)) {x4/x1,push(x4,s0)/s4} AT(box, x4, climb(push(x4,s0))) NIL {c/x4,push(c,s0)/s2} HB(s5) ? HB(grasp(s3)) ? ? HB(grasp(climb(s2))) HB(grasp(climb(push(c,s0)))) 第三章 一般搜索原理 消解原理 猴子摘香蕉問題的（修正）消解樹 2/27/2023 92 消解方法小結(jié) ? 求子句集，進行歸結(jié)，方法簡單 ? 通過修改證明樹的方法，提取回答 ? 方法通用 ? 求解效率低，不宜引入啟發(fā)信息 ? 不宜理解推理過程 第三章 一般搜索原理 消解原理 2/27/2023 93 一般搜索原理 The End. 第三章 一般搜索原理 2/27/2023 94 演講完畢，謝謝觀看！