【正文】 集 IC∪r 為根節(jié)點的推理樹，每個 tableau分枝 B為 I∪r 形式，I∈TP(IC) ， I稱為分枝的 IC部分，如果 r是不相容的，tableau是封閉的，即 tableau存在封閉分枝．由于 IC是相容的，因此一個 tableau的 IC部分永遠是不封閉的，只有 r和 IC相結合才能產(chǎn)生一個封閉的 tableau。 規(guī)則 1表示為 ?x?y(brother(x,y)??woman(x)) 事實表示為 sister(Mary,Bill) 作業(yè) 用歸結法證明 A1∧A 2∧A 3?B，其中 A1= (?x)((C(x)∧ ?D(x))?(?y)(G(x,y)∧E(y))) A2= (?x)(C(x)∧F(x)∧( ?y)(G(x,y)?F(y))) A3=?(?y)(D(x)∧F(x)) B= (?x)(E(x)∧ F(x)) 一階謂詞歸結推理 (5) 證明子句集 S={?P∨Q, ?Q, P}是不可滿足的。 ⑤ 如果某人是賊 ,而且他喜歡某物 ,則他就可能會偷竊該物。 表達式集合 {P(a,y), P(x,f(b))}是可合一的，其合一 ?為 ?={a/x, f(b)/y} 一階謂詞歸結推理 (1) 假設有以下前提知識： （ 1）自然數(shù)是大于零的整數(shù)； （ 2）所有整數(shù)不是偶數(shù)就是奇數(shù)； （ 3）偶數(shù)除以 2是整數(shù)。 Mike討厭 Tony所喜歡的一切東西，而喜歡 Tony所討厭的一切東西。當且僅當有一個 x0?D,使 P(x0)=F時，(?x)(P(x))=F。 tableau推理舉例 ((P→ ﹁ Q)∧( ﹁ R→P)∧Q)=R 證明：先將 ((P→ ﹁ Q)∧( ﹁ R→P)∧Q)∧ ﹁ R化為合取范式 (﹁ P∨ ﹁ Q)∧(R∨P)∧Q∧ ﹁ R (1) ﹁ P∨ ﹁ Q (2) R∨P (3) Q (4) ﹁ R (5) R P (6) ﹁ P ﹁ Q * * * 謂詞邏輯 :是命題邏輯的推廣，命題邏輯是謂詞邏輯的特殊情況。 Tableau擴展規(guī)則 ﹁ ﹁ Z Z ﹁ T F T ﹁ F ? ? ?1 ?2 ?1 ?2 Tableau有效性 定義： 一個命題公式集 S是可滿足的，如果某一布爾值映射到 S的每個成員都為 T. 一個tableau分支 ?是可滿足的，如果在個上面的命題公式集是可滿足的。 從而歸結是正確的推理規(guī)則。 結論： 我熱衷于玩撲克。 謂詞邏輯 : 1 命題邏輯 命題聯(lián)結詞及真值表 P ?P F T T F 否定： P Q P∨Q F F F F T T T F T T T T 析取： P Q P∧Q F F F F T F T F F T T T 合?。? F T F T F T T F F T T T P?Q P Q 蘊涵： F T F F F T T F F T T T P?Q P Q 等價： 命題聯(lián)結詞及真值表 合式公式 ： 命題演算的合式公式，規(guī)定為： （ 1） 單個命題變元本身是一個合式公式； （ 2） 如果 A是合式公式，那么 ﹁ A也是合式公式； （ 3） 如果 A， B是合式公式，那么 A∧B, A∨B ， A→B ，A?B都是合式公式； （ 4） iff 能夠有限次應用 (1)、 (2)、 (3)所得到的包含命題變元、聯(lián)結詞和括號的符號串是合式公式。 復合命題 ：兩個或幾個簡單命題用聯(lián)結詞聯(lián)結構成 的命題。 實例： 如果我學習，那么我數(shù)學不會不及格；如果我不熱衷于玩撲克，那么我將學習；但我數(shù)學不及格。 歸結推理規(guī)則 歸結過程就是對 S的子句求歸結式的過程： C1∧C 2 =R(C1,C2), R(C1,C2)是子句C1,C2的邏輯推論。 歸結推理舉例 ((P→ ﹁ Q)∧( ﹁ R→P)∧Q)=R 證明：先將 ((P→ ﹁ Q)∧( ﹁ R→P)∧Q)∧ ﹁ R化為合取范式 (﹁ P∨ ﹁ Q)∧(R∨P)∧Q∧ ﹁ R 建立子句集 S={﹁ P∨ ﹁ Q,R∨P,Q, ﹁ R} 歸結過程： (1) ﹁ P∨ ﹁ Q (2) R∨P (3) Q (4) ﹁ R (5) ﹁ P (1)(3)歸結 (6) P (2)(4)歸結 (7) □ (5)(6)歸結 tableau推理法（ 1） tableau定義 令 {A1,?,A n}為一命題公式的有限集合： 下列分支為 {A1,?,A n}的一個 tableau A1 … An 如果 T是一個 {A1,?,A n}的 tableau，對 T應用tableau擴展規(guī)則生成 T*，那么 T*仍然是一個 tableau。 完備性 ： 如果 X是一個重言式，那么 X有一個tableau證明過程。 (?x)(x是運動的） (?x)(P(x)):當且僅當對論域中的所有 x來說， P(x)均為真時方為真，這就是全稱量詞的定義。登山運動員不喜歡雨，而且任何不喜歡雪的人都不是滑雪運動員。 表達式集合 {E1,?,E k}稱可合一的，如果存在關于此集合的一個合一。 ④ 如果 Paul喜歡某物則 John也喜歡某物 。 求證：用歸結推理方法證明 Mary不是 Tom的兄弟。研究案情時，偵察員 A說：“趙和錢至少有一個人作案”；偵察員 B說：“錢和孫至少有一個人作案”；偵察員 C說：“孫和李至少有一個人作案”；偵察員 D說：“趙和孫至少有一個人與此案無關”；偵察員 E說：“錢和李至少有一個人與此案無關”。 3 1968 Smullyan 利用模型存在定理證明了 tableau方法。 研究的意義 人工智能研究的基礎工作，許多重要的人工智能系統(tǒng)，都以推理系統(tǒng)為其核心部分。在 ?規(guī)則基礎上給出識別 ?公式方法 ， 提 出 了 含 ? 公 式 的tableau推理的改進策略 ， ?公式不再需要實例化 ， 縮短了tableau的證明過程 。 令 {A1,A2,… ,An}為公式的有限集合 。 (3)本文工作 對于 ?公式，通過 skolem否定范式轉(zhuǎn)換后的公式中不再存在。(y 令 R為識別 ?公式的方法 ， 帶分枝B1,? ,Bk的自由變量 tableau T是封閉的 ， 當且僅當存在替換 σ1, ? ,σ k使得： ⑴ 對于 1≤i≤k ，公式 Fi,172。 利用的識別 ?公式的方法，等式⑹被識別為關于x1的 ?公式，因此 x1不再需要實例化，例子的tableau過程中的⑽⑾⑿可以刪除，通過替換{a/x2}即可封閉。] ? [t180。 第一階段是在處理等詞之前 ， 應用 tableau擴展規(guī)則 ， 將所有的 tableau擴展完成 ， 在這個過程中要求對 ?規(guī)則應用次數(shù)進行限制 。 E(B)={g(f(x))≈c ,f(x)≈g(x)} P(B)={g(g(a))≠g(f(b))} Tableau的第二階段轉(zhuǎn)換成計算 g(g(a))和 g(f(b))的合一元素。 改進啟發(fā)式算法，提高計算等價類的速度。 ⑴ 如果 (Q(?))1(S)=U(F)，則 S(?x)?(x)是可滿足的當且僅當對于新的 Skolem常數(shù) c， F?(c)是可滿足的。 ⑶ 對于任何 i∈N 和分配格 L: (Q－１ (Π))({i})=(U( ?m))∩(D( ?i)∪{ ?})，其中 Mi是 MI(L)∩ ?i中的最小元素。 利用四值布爾集格，對集合 {⊥} ， {f}，{⊥,f} 可以簡化表示為： {t}?(d) {f, ?}?(c) {f}?(c) {⊥}?(c) {f}?(c) {⊥,f}?(c) {⊥}(Πx) ?(x)的擴展分枝由 10個減少為 2個。 ⑺ 如果 L是分配格并且 i∈JI(L) ，那么 (Q－１ (Σ))( ?i)=U(?i)。 2 1 2 1 將含量詞的 tableau方法與布爾集格相結合 ， 簡化了 tableau的擴展分枝 ， 在本章中我們稱之為布爾剪枝 。 通過對布爾剪枝方法的進一步探討 ， 建立了一類特殊一階多值邏輯正則公式的更為簡捷的 tableau推理方法 ， 該方法使得含量詞的一階多值邏輯 tableau推理類同于經(jīng)典邏輯 tableau方法 。 提出利用等式合一處理含等詞 tableau方法 ， 將 tableau擴展分成兩個階段 。 基本思想： 完備性： 如果公式 ?是不可滿足的， q足夠大，那么 T是 T2封閉的。 （ 2）問題提出 等式合一問題 E， s， t包含形如 (?x1) ? (?xn)(l≈r) 的等式的有窮集合 E、 項 s和 t。 含等詞的 tableau方法研究現(xiàn)狀 問題提出 本文工作 實例對比分析 小結 Jeffrey方法 （ 1）含等詞的 tableau方法分析 t≈s s≈t ?[t] ? [t] ?[s] ? [s] Jeffrey含等詞擴展規(guī)則 存在問題 無關公式的數(shù)目隨著謂詞元數(shù)的增加呈冪指數(shù)增長 擴展規(guī)則是對稱的，它的應用不受限制。 這樣會使tableau過程縮短 ， 搜索空間減小 。 令 Γ 為理論 ， φ 為 tableau T的一個分枝 B上的公式 ， 對于變量 x,通過向 T的分枝B中增加 (?x)φ 而得到 tableau T’ ,如果T╞ Γ T’ ,那么對于 x， 在 B上公式 φ 是 γ 公式 。 (1)研究現(xiàn)狀 (2)問題提出 (3)本文的工作 (4)實驗對比 如果一個 tableau分枝 B包含一個公式 P(x)，在 tableau過程中 ， x必然出現(xiàn)在某些分枝上 ，為了封閉這些分枝需要多次對 x進行實例化 (?P(a)∨ ?P(b))∧(( ?x)P(x)) ?P(a)∨ ?P(b) (?x)P(x) P(y) ?P(a) ?P(b) P(a)a/y P(b) b/y (1) 研究現(xiàn)狀 在 tableau證明中 , ?公式對其中包含的自由變量需要進行多次不同的實例化。 （ 1）研究現(xiàn)狀 ?規(guī)則要求被 Skolem化的函數(shù)符號是新的 ， 且函數(shù)中包含分枝中出現(xiàn)的所有自由變量 ． 顯然 ， 由于 ?規(guī)則的不確定性以及 ?規(guī)則的限制 ， 可使一個簡單的證明變得很復雜 ， 延遲了 tableau的封閉時間 。 ⑶ 在增添擴展規(guī)則的 tableau方法的基礎上提出了一種新的含等詞tableau方法 —— 等式合一方法 。 (1)相關技術和策略的研究 非相關部分剪枝技術 由 Oppacher提出的 tableau壓縮技術。 7 1986 Bryant 提出決策圖 tableau方法，能表達一個很大的可滿足的公式模型。 （ 3） 通用性和直觀性：對于不同的邏輯系統(tǒng) ，使用相同的 tableau規(guī)則 ， 只是對公式構造集進行擴展 ， 使之更接近相應的邏輯系統(tǒng) 。 設 C1=P(x)∨ ?Q(x), C2=Q(g(x))，求其二元歸結式。 (2)將已知事實表示成謂詞公式 ,并化成子句集 ① theif(John) ② likes(Paul,wine) ③ likes(Paul,cheese) ④ ?likes(Paul,y)∨likes(John,y) ⑤ ?theif(x)∨ ?likes(x,y)∨may_steal(x,y) ⑥ ?may_steal(John,Z)∨ANSWER(Z) (3)歸結 ⑦ ?theif(John)∨ ?likes(John,y)∨ANSWER(y) ⑤⑥ 歸結 ,?={John/x, y/z} ⑧