[工學]哈工大人工智能課件chpt(存儲版)

　　

【正文】 ? 子句 (clause)：文字的析取稱為子句 ? 合取范式：形如 A1∧ A2∧ … ∧ An的公式 ， 其中 A1～ An均為子句 ? 前束范式：形如 (Q1x1… Qn xn)M(x1… xn)的公式 ， M中不再含有量詞 ， Q是量詞 ? Skolem標準形：在前束范式中消去存在量詞后得到的公式 第 4章 消解法 15 消去存在量詞 ? 消去存在量詞的步驟： (1)若存在量詞不在任何全稱量詞之后 ， 則公式中被存在量詞量化的變量以某個不同于公式中任何其他常量名字的常量 c代替 ， 并消去存在量詞； (2)若存在量詞在 k個全稱量詞之后 ， 則公式中被存在量詞量化的變量用被前 k個全稱量詞量化的變量 x1～ xk的某個函數 f(x1～ xk)的形式代替 ，f的名字不同于公式中任何其他函數的名字 ，但對函數形式沒有要求；然后消去存在量詞 / 函數 f稱為 Skolem函數 第 4章 消解法 16 公式轉化為子句集的步驟 (1) ? 公式 A化為子句集 S， 其實現步驟共 9步 ，如下： (1)消去等價和蘊含符號：蘊含轉化為析取 (2)將否定符號轉移到每個謂詞之前：應用狄摩根定律 (3)變量標準化：約束變量各不相同 (4)公式化為前束型：全部存在量詞和全稱量詞移到公式的最前面 /得到的兩部分稱為前綴和母式 第 4章 消解法 17 公式轉化為子句集的步驟 (2) (5)消去存在量詞：存在量詞不受全稱量詞約束 ，則變量用常量替換 /如果存在量詞受全稱量詞約束 ， 則使用 Skolem函數替換相應變量 ——得到 Skolem標準形 (6)母式化為合取范式：外層連接符全部是合取 ，里層連接符全部為析取 (7)去掉所有全稱量詞 (8)母式化為子句集：每個合取項間的合取符號 (∧ )用逗號代替 ， 即得子句集 (9)子句變量標準化：每個子句中的變量各不相同 第 4章 消解法 18 合一算法 ? [定義 ]置換 (或代換 )：設 x1～ xn是 n個變量，且各不相同， t1～ tn是 n個項 (常量、變量、函數 )， ti≠xi，則有限序列 {t1/x1, t2/x2 …t n/xn}稱為一個置換 ? 置換可以作用于謂詞公式，也可以作用于項。 ? [定義 ]因子：若子句 C中的多個文字具有mgu， 則 [C?]稱為 C的一個因子 。 第 4章 消解法 44 歸類算法 (3) ? 注意： Uk+1=Φ表明 Uk和 W中已不存在可消解的子句 ， 所以沒有 R(C1, C2)， 其中 C1∈ Uk, C2∈ W 第 4章 消解法 45 歸類算法舉例 ? 例子： 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不空繼續 (3)U2顯然包含 □ ， 因為 Q(f(h(b)), a)∈ U1而 ﹁ Q(f(h(b)), a)∈ W 可消解為 □ ， 同樣 ﹁ P(h(b))∈ U1 而P(h(b))∈ W可消解為 □ 。其消解過程可由下圖說明 第 4章 消解法 S ’ S ’ ○﹁ P ∨ Q ○﹁ P ∨﹁ Q ○ P ∨﹁ Q ○﹁ P ∨﹁ Q ○ ﹁ P ○﹁ Q ○ P ∨ Q ○ Q ○ □50 動態支持集消解 ? 判斷 S―S’ 是否可滿足，需要花費時間，所以要尋找更好的策略。 ★ 第 4章 消解法 S2 ﹁ P ○ ○ P ∨﹁ Q ﹁ Q ○ ○ Q ∨﹁ R ﹁ R ○ ○ R □ ○54 單元消解 ? [單元消解定義 ]在動態支持集消解定義中令 Sn2={Sn 中所有單子句和單因子 }，則此策略稱為單元消解策略(也叫單項消解 ) / 這樣，每次參加消解的一方總有一個是單項 ? 例 4 ： S={P∨ Q,﹁ P∨ R,﹁Q∨ R,﹁ R}， 其消解過程如圖所示 。 這兩個圖的語義樹都是完備的 第 4章 消解法 ? P ,R ? P ? R ? ? ? Q ? Q Q ,R ? Q ? R P ? P ? ? ? ? ? ? ? R ? R Q ? Q Q ? Q Q ? Q ? ? ? ? ? ? ? ?67 語義樹和 H解釋 ? 因為一般 H基是個無窮集合，所以其對應的語義樹也是無限的 ? 因為在完備語義樹的每一條路徑上都有 S的全部原子 (或負原子 )，所以對這些原子公式的真值判定就能決定 S的一個解釋 ? 對于有限完備語義樹來說，如果 N是一個葉節點，則 I(N)便是 S的一個 H解釋 / 這樣，S的不可滿足性就與完備語義樹路徑的真值計算聯系起來 第 4章 消解法 68 封閉語義樹 [定義 ]基例：如果 S的某個子句 C中所有變量符號均以 S的 H域的元素 (常量 )代入時，所得的子句 C’稱為 C的一個基例 [定義 ]否節點：如果語義樹節點 N的從根節點到 N的路徑 I(N)使 S的某個子句的某個基例為假，而其父輩節點不能判斷此事實 (即 I(N)是使基例為假的最小路徑 )，則稱 N為否節點 (或失敗節點 ) [定義 ]封閉語義樹：如果一棵完全語義樹的每個分枝上都有一個否節點，則稱為封閉語義樹 第 4章 消解法 69 封閉語義樹例子 (1) ? 例：設子句集 S={﹁ P(x)∨ Q(x),P(f(x)), ﹁ Q(f(x))} 包括 3個子句 : ﹁ P(x)∨ Q(x), P(f(x), ﹁ Q(f(x)) 則 H∞={a, f(a), f(f(a)), …} H基 ={P(a), Q(a), P(f(a)), Q(f(a)), …} ? 其封閉語義樹如下圖所示 第 4章 消解法 70 封閉語義樹例子 (2) 第 4章 消解法 ● N0 P(a) ﹁ P (a) ● N1 / 1 ● N1 / 2 Q (a) ﹁ Q( a) Q(a ) ﹁ Q (a) ● N2 / 1 ★ N2 / 2 ● N2 / 3 ● N2/4 P ( f ( a ) ) P ( f ( a ) ) ● N3 / 1 ★ N3 / 2 ● N3 / 5 ★ N3 / 6● N3 / 7 ★ N3 / 8Q ( f ( a ) ) Q ( f ( a ) ) ★ ★ ★ ★ ★ ★ N4/ 1 N4 /2 N4 / 9 N4 / 1 0 N4 / 1 3 N4 / 1 471 封閉語義樹例子 (3) ? 封閉語義樹中每個否節點用 ★ 表示 ? 在上圖中 ， 每個否節點的路徑為： ? I(N2/2)={P(a),﹁ Q(a)}， 使 (﹁ P(a)∨ Q(a))=F； ? I(N3/2)={P(a),Q(a),﹁ P(f(a))}， 使 P(f(a))=F； ? I(N4/9)={﹁ P(a),Q(a),P(f(a)),Q(f(a))}，使 Q(f(a))=F如此等等 ? 上述每個路徑所代表的解釋已經使 S的某個子句為假 ， 因此再擴充路徑仍然只能使同一子句為假 ， 所以沒有擴充 、 延伸的必要 □ 第 4章 消解法 72 有限封閉語義樹 ? 上例說明 ， 從不可滿足的角度來說 ， 對于無限完備語義樹只需搜索到一個否節點 ，則該分枝即被證明為不可滿足 。設 I是S的任一解釋，則其落在 T的某個分支 B上， B上