【文章內(nèi)容簡介】 的變量可以在量詞作用范圍內(nèi)用另外變量代替。我們可以對變量適當?shù)馗拿?, 使每一個量詞所約束的變量都有不同的名字 . 例如 , 謂詞公式 （ ?x） P（ x） ∨ (?x) Q（ x） 改寫成 （ ?x） P（ x） ∨ (?y )Q（ y） . 4. 刪除公式中的存在量詞 . 例如 ,謂詞公式 （ ?x)(?y)P（ x, y) 在刪去存在量詞之后 , 變成 （ ?x)P（ x, f(x)) , 在刪去存在量詞之后 , 這個存在量詞所約束的變量的每次出現(xiàn)都用一個函數(shù)代替 , 這個函數(shù)的自變量是約束范圍包含刪除的存在量詞的所有全稱量詞限制的變量 . 這個函數(shù)也叫做 Skolem函數(shù) . 把刪除存在量詞 ,將存在量詞限制的變量用對應(yīng)的 Skolem函數(shù)代替的過程叫做 Skolem化過程 . 結(jié)果叫做 Skolem范式 . )]()()()[~( xQxxPx ???吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 例 將下式化為 Skolem標準型 : ～ (（ ?x) (?y )P(a,x,y) → ( ?x )( ～（ ?y） Q(y,b) →R(x))) ～ (～ （ ?x) (?y )P(a,x,y) ∨ ( ?x )( ～ ～ （ ?y） Q(y,b) ∨ R(x))) （ ?x) (?y )P(a,x,y) ∧ ～ (?x )(（ ?y） Q(y,b) ∨ R(x))) （ ?x) (?y )P(a,x,y) ∧ ( ? x )(（ ? y） ～ Q(y,b) ∧ ～ R(x))) （ ?x) ((?y )P(a,x,y) ∧ ( （ ? y） ～ Q(y,b) ∧ ～ R(x))) （ ?x) ((?y )P(a,x,y) ∧ ( （ ? z） ～ Q(z,b) ∧ ～ R(x))) （ ?x) (?y ) （ ? z） ( P(a,x,y) ∧ ～ Q(z,b) ∧ ～ R(x)) （ ?x) （ ? z） ( P(a,x,f(x)) ∧ ～ Q(z,b) ∧ ～ R(x)) （ ?x) ( P(a,x,f(x)) ∧ ～ Q(g(x),b) ∧ ～ R(x)) 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (子句集 ) 文字 我們把命題原子稱作正文字， 例如 P(x), Q(y,b), R(w,c)?., 等等， 把帶有非符號的命題原子叫做負文字，例如 ~P(y), ~Q(a,b), ~R(x,y,z)?., 等等，把正文字和負文字統(tǒng)稱為文字。 子句 單個文字， 文字的析取構(gòu)成的命題邏輯公式叫做子句。 例如， P, ~Q(x) , P(x) ∨ ~ Q(y,b), 都是子句。 子句集 若干子句的集合 . 一個命題邏輯公式可以采用如下方式轉(zhuǎn)換成等價的子句的合取形式 , 即合取范式： 1. 利用等價公式 P←→ Q =( P→Q)∧ (Q←P) 和 P→Q=~P∨Q刪去公式中的 ←→ 符號和 → 符號 . 2. 利用 De Man 律把所有的否定符號移到每個原子之前 . 3. 利用分配律得到子句的合取形式 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (子句集 ) 4. 把公式變換成 Skolem標準型 . 5. 把 Skolem標準型中子句提出 .表示為集合形式 . 定理 公式 G是不可滿足的 , 當且僅當其子句集 S是不可滿足的 , 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (替換與合一 ) 在命題邏輯歸結(jié)中 , 需要兩個子句有互補文字 , 這兩個文字除了否定符號之外是完全相同的 . 但在謂詞邏輯中包含變量 , 而變量可以指定成其他任何常量 , 變量 , 或者函數(shù)項 , 可以在指定后再實施歸結(jié) , 因此即使兩個項不完全相同 , 也可能進行歸結(jié) . 例如 , 設(shè)有謂詞邏輯子句 c1和 c2 ， c1=P(x)∨ ~ Q(x,y) c2= ~ P(f(a))∨ R(x,b), 表明上看來沒有互補文字 , 但是 , 如果把 c1和 c2中的 x都指定成 f(a), 則有互補對 P(f(a)) 和 ~ P(f(a)), 這時 c1和 c2 就可以歸結(jié)得到 ~ Q(f(a),y)∨R(f(a),b), 這種為變量的指定稱為替換 , 本節(jié)我們先介紹替換 . 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (替換與合一 ) 替換是如下形式的偶對組成的集合 : s = { t1/ v1, t2/ v2,…, tn/ vn, } 其中 t1, t2,…, tn 是項 , v1, v2,…, vn 是彼此不同的變量 , ti中不包含變量 vi. 例如 , 下面的 4個偶對集合是 4個替換 : s1 = {z/x, w/y} s2 = {A /y} s3 = {g(z)/x, A/y} s4 = {C/x, A/y} 把替換 s用于表達式 E是把 E中變量 vi的每次出現(xiàn)都用對應(yīng)的項 ti 代替 (i =1,2,…, n ), 成為表達式 E的替換例，記為 Es. 例如， 設(shè) E = P(x, f(y), B), 則 Es1 = P(z, f(w), B) Es2 = P(x, f(A), B) Es3 = P(g(z), f(A), B) Es4 = P(C, f(A), B) 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (替換與合一 ) 設(shè) s1和 s2 是兩個替換， s1= { t1/ x1, t2/ x2,?, tn/ xn } s2 = {u1/ y1, u2/ y2,?, un/ yn } 我們可以利用 s1和 s2組合產(chǎn)生一個新的替換， 這種組合相當于引進替換中的一種運算， 記為 s1s2, 其結(jié)果是把 s2用在 s1的所有的項 ti 上 (i =1,2,?, n ) ， 然后把 s2中加進去， 得到 { t1s2/ x1, t2s2/ x2,…, tns2/ xn, u1/ y1, u2/ y2,…, um/ ym} 再刪除一些不符合替換要求的偶對 :tis2=xi, s2變量在 s1出現(xiàn)的偶對。 例如， 設(shè)： s1= { f(y)/ x , z/y}, s2 = { a/ x, b/ y, y/ z } 則 從集合中 { f(b)/ x , y/y, a/ x, b/ y, y/ z } 刪除 y/y， a/ x， b/ y,得到 s1s2={ f(b)/ x , y/ z } 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (替換與合一 ) 替換的復(fù)合運算滿足結(jié)合律， 不滿足交換律。 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (替換與合一 ) 設(shè) {E1, E2, ?, En} 是一個表達式集合，如果存在一個替換 s，把 s用于這個表達式集合的替換例集合滿足 E1s = E2s= ,?,= Ens, 則稱該表達式集合是可合一的， 而 s稱為該表達式集合的合一替換。 例如， 設(shè) E1=P(x, f(y),B), E2=P(x, f(B),B), s={ A/ x, B/ y}, 則容易驗證 E1s = E2s= P(A, f(B),B) 因此 E1和 E2是可合一的。 盡管這個替換 s可以使 E1和 E2合一， 但 s并不是最簡單的。 在謂詞邏輯歸結(jié)中， 我們總希望使用最簡單的合一。 因此下面給出最一般合一的概念。 設(shè)設(shè) {E1, E2, ?, En} 是一個表達式集合， g是該表達式集合的一個合一替換 , 如果對任何合一替換 s, 都有替換 s’, 滿足 s = gs’ ， 則稱 g是 {E1, E2, ?, En} 的最一般合一替換。在我們上述的例子中，最一般合一替換是個 g={ B/ y}, s = g {A/x}. 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (替換與合一 ) 求最一般合一算法 1. 令 W={F1, F2} 2. 令 k=0, W0=W, s0={} 3. 如果 Wk已合一 , 停止 , sk=mgu, 否則 , 找不一致集合 Dk, 4. 如果 Dk中存在元素 vk和 tk, 并且 vk不出現(xiàn)在 tk中 , 轉(zhuǎn) 5, 否則不可合一 . 5. sk+1=sk{tk/vk}, Wk+1=Wk{tk/vk} 6, k=k+1, 轉(zhuǎn) 3. 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (替換與合一 ) 例 , 設(shè) f1=P(a,x,f(g(y))), F2=P(z, f(a), f(u)) 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (歸結(jié)式 ) 謂詞邏輯歸結(jié)式 設(shè) c1, c2是兩個子句， 為敘述方便， 我們假定子句都寫成文字集合的形式， 而把這些集合中文字的關(guān)系約定為析取。 c1={L1}∪ D1, c2={~L2}∪ D2 , 其中 L1 ， L2是可合一的原子， 假設(shè)它們的最一般合一是 s， D1和 D2 為子句． 則 c1, c2的歸結(jié)式 r 為： [(c1 ―{L1 }) ∪ (c2―{~L2})] s 在對子句實施歸結(jié)之前， 為了避免不必要的混淆，我們對子句中的變量進行改名， 使得各子句中的變量都使用不同的名字。 例如， 假設(shè)我們想要對兩個子句 P(x) ∨ Q(f(x)) 和 R(g(x)) ∨ ~ Q(f(A))實施歸結(jié)， 我們先把第二個子句中變量進行改名， 得到 R(g(y)) ∨ ~ Q(f(A)), 然后通過歸結(jié)得到 P(A) ∨ R(g(y)), 這種變量改名的過程也叫做變量的分離標準化。 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (歸結(jié)式 ) 例 (1) c1= P(x) ∨ Q(x,y) 和 c2=~ P(a) ∨ ~ R(b, z) 它們的歸結(jié)式 R(c1, c2)= Q(a,y) ∨ ~ R(b, z) 例 (2) c1= P(x, y) ∨ Q(x) ∨ R(x) 和 c2=~ P(a, z) ∨ ~ Q(b) 它們的歸結(jié)式 R(c1, c2)= Q(a) ∨ R(a) ∨ ~ Q(b) 或者 P(b, y) ∨ R(b) ∨ ~ P(a, z) 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (歸結(jié)過程 ) 謂詞邏輯中歸結(jié)方法的主要思想與命題邏輯相同。 假設(shè)我們想從公式集合 SF = {f1, ? , fn} 出發(fā)證明公式 g, SF稱為前提集合， g稱為結(jié)論，我們先把 f1, ? , fn 和 ? g 轉(zhuǎn)換成子句集 Cf1, ? , Cfn 和 C?g, 設(shè) SC = Cf1 ? , ? , ? Cfn ? C?g 為初始子句集，然后在 SC的子句間實施歸結(jié)，不斷地加入新的歸結(jié)式，然后繼續(xù)歸結(jié)，當子句集中出現(xiàn)了空子句時， 我們就證明了 SF ? g, 即證明了 g是 SF的邏輯結(jié)果。 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (歸結(jié)過程 ) 例 假設(shè)任何任何通過計算機考試并獲獎的人都是快樂的， 任何肯學(xué)習(xí)或幸運的人都可以通過所有的考試， 張不肯學(xué)習(xí)但他是幸運的， 任何幸運的人都能獲獎。 求證： 張是快樂的。 R1:任何任何通過計算機考試并獲獎的人都是快樂的 （ ?x)((Pass(x, puter) ∧ Win(x, prize)) →Happy(x)) R2:任何肯學(xué)習(xí)或幸運的人都可以通過所有的考試， （ ?x) （ ?y) ((Study(x) ∨ Lucky(x)→ )((Pass(x, y)) R3:張不肯學(xué)習(xí)但他是幸運的 ~Study(zhang) ∧ Lucky(zhang) R4:任何幸運的人都能獲獎 （ ?x) (Lucky(x)→ Win(x, prize)) 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (歸結(jié)過程 ) 要證的結(jié)果：張是快樂的。 Happy(zhang) 轉(zhuǎn)換為子句 1. ~ Pass(x, puter) ∨ ~ Win(x, prize)) ∨ Happy(x)) 2. ~ Study(y) ∨ Pass(y, z) 3. ~ Lucky(u) ∨ Pass(u, v) 4. ~Study (zhang) 5. Lucky(zhang) 6. ~ Lucky(x) ∨ Win(x, prize) 7. ~ Happy(zhang) 吉林大學(xué)珠海學(xué)院計算機科學(xué)與技術(shù)系 人工智能 謂詞歸結(jié)原理 (歸結(jié)過程 ) 8. ~ Pass(w, puter) ∨ Happy(w))∨ ~ Lucky(w) 1,6 {w/x} 9.