【正文】 ， 在這個過程中要求對 ?規(guī)則應(yīng)用次數(shù)進行限制 。 第二階段是處理等詞 ，通過適當(dāng)?shù)氖侄?， 限制等詞的使用 ， 以避免無關(guān)公式的產(chǎn)生 。 分階段 tableau方法不需要在等詞應(yīng)用規(guī)則和其它擴展規(guī)則之間轉(zhuǎn)換 ， 因此在第一階段完成以后 ， 許多公式不再需要 。 從第二階段開始只需要考慮等式 、 不等式以及潛在的封閉原子對 ， 這樣使含等詞的 tableau在一個更適合的數(shù)據(jù)結(jié)構(gòu) P(B)和 E(B)下進行 。 基本思想： 完備性： 如果公式 ?是不可滿足的， q足夠大，那么 T是 T2封閉的。 可靠性： 如果 T是 T2封閉的，那么公式 ?是不可滿足的。 T是關(guān)于公式 ?的 tableau， q是 ?規(guī)則應(yīng)用的限定次數(shù)， Tableau T是 T2封閉的，當(dāng)存在一個基替換 ?，對于 T上的每一個分枝 B，存在一個析?。?t1≠s 1∨ ? ∨t n≠s n） ∈ P(B)使得 1≤i≤n ， [ti?]B=[si?]B. 定 義 定 理 begin t={tid} n=1 while n=N do begin 將 t 中不被另一元素包含的所有元素加入到 Θn中 s?= H(t) while flag do begin s??加入到集合 Θn中 ?是 s和等式 G∈ E(B)一端的 MGU if ?存在 then flag=true else flag=false n=n+1 end end end 算法 (計算集合 t的等價序列的近似算法 ) 輸入 ：項 t、 等式集合 E(B)、 n的最高次數(shù) 輸出 ：項 t的等價序列集合 t (?x)[g(f(x))≈c∧(f(x)≈g(x)∨ ?)]→g(g(a))≈g(f(b)) 為重言式．其中 ?為不可滿足的任意公式． tableau第一階段的擴展如下： F (?x)[g(f(x))≈c∧(f(x)≈g(x)∨ ?)]→g(g(a))≈g(f(b)) √ T (?x)[g(f(x))≈c∧(f(x)≈g(x)∨ ?)] √ F g(g(a))≈g(f(b)) T g(f(x))≈c∧(f(x)≈g(x)∨ ?) √ T g(f(x))≈c T f(x)≈g(x)∨ ? √ T f(x)≈g(x) T ? * 后面標(biāo)注 “ √ ” 的為不再使用的公式 ， 第一階段完成后 ，tableau擴展已經(jīng)完成 ， 但 tableau沒有封閉 。 例 ： 證明公式 設(shè)未封閉分枝為 B， B轉(zhuǎn)換成集合 E(B)和 P(B)。 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))的合一元素。 ① g(f(x))≈c ② f(x)≈g(x) g(g(a)) g(f(b)) ① g(f(x))≈c ② f(x)≈g(x) g(g(a)) g(f(b)) f(g(a)){g(a)/x} g(f(a)){a/x} P(B) E(B) 第一步 第二步 ① g(f(x))≈c ② f(x)≈g(x) g(g(a)) g(f(b)) f(g(a)){g(a)/x} f(f(b)){f(b)/x} g(f(a)){a/x} g(g(b)){b/x} cid ① g(f(x))≈c ② f(x)≈g(x) g(g(a)) g(f(b)) f(g(a)){g(a)/x} f(f(b)){f(b)/x} g(f(a)){a/x} g(g(b)){b/x} c{a/x} cid 第三步 第四步 （ 1）如果使用 Fitting方法證明同一公式為重言式，?公式的使用次數(shù)必須提高。 （ 2）在同一啟發(fā)搜索算法下，證明不等式g(g(a))≠g(f(b)) 的不可滿足性，將產(chǎn)生 15個中間等式，并需要幾次的自由變量替換。 （ 3）如果使用 Jeffrey方法證明同一公式為重言式，等式規(guī)則的應(yīng)用次數(shù)依賴于使用等式的次序，最好的情況下只需要 2個分枝即封閉，然而在較差的情況下可以產(chǎn)生幾百個分枝。 提出利用等式合一處理含等詞 tableau方法 ， 將 tableau擴展分成兩個階段 。 第一階段是在處理等詞之前 ， 應(yīng)用 tableau擴展規(guī)則 ，將所有的 tableau擴展完成 ， 在這個過程中要求對 ?規(guī)則應(yīng)用次數(shù)進行限制 。 第二階段是處理等詞 ， 通過提取等式合一問題并求解解替換封閉 tableau， 在啟發(fā)式的幫助下計算等價類的方法 ， 限制等詞的使用 ， 以避免無關(guān)公式的產(chǎn)生 ， 在效率和實現(xiàn)上都有較大的提高 。 （ 5）小 結(jié) 一是 二是 將計算等價類的結(jié)果以樹的結(jié)構(gòu)進行存儲 ， 利用樹的特點 ， 進行搜索的優(yōu)化 ， 提高推理效率 。 改進啟發(fā)式算法，提高計算等價類的速度。 (1)含量詞的一階多值邏輯 Tableau (2)問題提出 (3)利用布爾集格對 tableau方法的改進 (4)含廣義量詞的四值邏輯 tableau實例 (5)實例分析 (6)多值邏輯正則公式的 tableau方法 (7)小結(jié) (Q(?))1(S)={I???I?N， Q(?)(I)?S} (Q(?))1({0})= {{0},{0, },{0,1},{0, ,1}} 2 1 2 1 擴展規(guī)則： 符號引入： 含量詞的 tableau方法是由 Carnielli（ 1987） 引入 ， 后來由 Zabel(1993)在理論上找到了可滿足的擴展規(guī)則 ， 并給出了可靠性和完備性的證明 。 然而對于自動定理證明來說 ， 其實現(xiàn)難度非常大 ， 為此找出一種擴展分枝更少的有效推理方法 。 提出了布爾剪枝方法 ， 將帶符號的公式與集合的上集／下集聯(lián)系起來 ， 使含量詞的一階公式的擴展規(guī)則大大簡化 。 通過對布爾剪枝方法的進一步探討 ， 建立了一類特殊一階多值邏輯正則公式的更為簡捷的 tableau推理方法 ， 該方法使得含量詞的一階多值邏輯 tableau推理類同于經(jīng)典邏輯 tableau方法 。 在多值邏輯中 例： 在一階三值 Kleene邏輯中，可以對{0}(?x)?(x)進行擴展，其中 (Q(?))1({0})= {{0},{0, },{0,1},{0, ,1}}。擴展結(jié)果如下： {0}?(c) {0}?(t1) {0}?(c) { }?(d) {0, }?(t2) {0}?(c) { }?(d) {1}?(e) {0, ,1}?(t3) {0}?(c) {1}?(e) {0,1}?(t4) 2 1 2 1 2 1 2 1 2 1 2 1 {0}(?x)?(x) 定義 F， ??F?N， 產(chǎn)生的關(guān)于布爾集格 2N的集合的上集為 U(F)={X? X?N,X∩F ??}。 定義 I，??I?N， 產(chǎn)生的關(guān)于布爾集格 2N的集合的下集為D(I)={X ?X?N,??X?I}。 ⑴ 如果 (Q(?))1(S)=U(F)，則 S(?x)?(x)是可滿足的當(dāng)且僅當(dāng)對于新的 Skolem常數(shù) c， F?(c)是可滿足的。 ⑵ 如果 (Q(?))1(S)=D(I)，則 S(?x)?(x)是可滿足的當(dāng)且僅當(dāng)對于所有的基項 t， I?(t)是可滿足的。 設(shè) N為有窮真值集， S?N， 定理 定義 例子中 ，一階三值 Kleene邏輯中， 因為 (Q(?))1({0})=U({0})={{0},{0, },{0,1},{0, ,1}}， 因此規(guī)則可簡化為： {0}(?x)?(x) {0}?(c) 另外，因為 (Q(?))1({0})= D({0})={{0}}， 因此規(guī)則 {0}(?x)?(x) {0}?(t) 是成立的。這一結(jié)論也是與經(jīng)典情況一致的。 2 1 2 1 將含量詞的 tableau方法與布爾集格相結(jié)合 ， 簡化了 tableau的擴展分枝 ， 在本章中我們稱之為布爾剪枝 。 在效率和實現(xiàn)上都有較大的提高 時間效率 空間效率 Zabel方法 O(nk) O(n*k) 布爾剪枝方法 O(n*k) O(n) 例：考慮真值集合 FOUR={⊥ ,f,t,?}，定義量詞 Π ， Q(Π )= ，這里 為格中的交操作。 ⊥ f t {⊥,f} {} {⊥} {f} {t} {?} {⊥,t} {f,t} {⊥,?} {f,?} {t,?} {⊥,f,t} {⊥,f,?} {⊥,t,?} {f,t,?} FOUR 四值布爾集格 四值邏輯格結(jié)構(gòu) ? 以 {⊥} 為例， tableau擴展結(jié)果如下： {⊥}?(c) {⊥}?(c) {⊥}?(c) {f}?(c) {⊥}?(c) {⊥}?(c) {⊥}?(c) {⊥}?(c) {f}?(c) {⊥}?(c) {f}?(d) {t}?(d) {t}?(d) {?}?(d) {f}?(d) {f}?(d) {t}?(d) {t}?(d) {f}?(d) {t}?(e) {?}?(e) {?}?(e) {?}?(e) {t}?(e) {?}?(f) {⊥}(Πx) ?(x) Q(Π)= ? Q(Σ)= ? 設(shè) L= N, ?,? 為真值有窮集合 N上的格，定義分布量詞 Π 和 Σ 如下： 則有下列式子成立： 定 理 ⑴ 如果 i∈MI(L) ，那么 (Q－１ (Π))({i})=U({i})∩(D( ?i)∪{ ?})。 ⑵ 如果 L是分配格并且 i∈MI(L) ，那么 (Q－１ (Π))( ?i)=U(?i)。 ⑶ 對于任何 i∈N 和分配格 L: (Q－１ (Π))({i})=(U( ?m))∩(D( ?i)∪{ ?})，其中 Mi是 MI(L)∩ ?i中的最小元素。 ⑷ 對于任何 i∈N 和分配格 L: (Q－１ (Π))( ?i)=U(?m)，其中 Mi是 MI(L)∩ ?i中的最小元素。 ⑸ 對于任何 i∈N ： (Q－１ (Π))( ?i)=D(?i)。 ⑹ 如果 i∈JI(L) ，那么 (Q－１ (Σ))({i})=U({i})∩(D( ?i)∪{ ?})。 ⑺ 如果 L是分配格并且 i∈JI(L) ，那么 (Q－１ (Σ))( ?i)=U(?i)。 ⑻ 對于任何 i∈N 和分配格 L: (Q－１ (Σ))({i})=(U( ?j))∩(D( ?i)∪{ ?})，其中 Ji是 JI(L)∩ ?i中的最小元素。 ⑼ 對于任何 i∈N 和分配格 L: (Q－１ (Σ))( ?i)=U(?j)，其中 Ji是 JI(L)∩ ?i中的最小元素。 ⑽ 對于任何 i∈N ： (Q－１ (Σ))( ?i)=D(?i)。 利用四值布爾集格，對集合 {⊥} ， {f}，{⊥,f} 可以簡化表示為： {t}?(d) {f, ?}?(c) {f}?(c) {⊥}?(c) {f}?(c) {⊥,f}?(c) {⊥}(Πx) ?(x)的擴展分枝由 10個減少為 2個。 {⊥}(Πx) ?(x) {f}(Πx) ?(x) {⊥,f}(Πx) ?(x) (Q(Π)) 1({⊥})= ?{f,t}∪ ?{⊥} (Q(Π)) 1{{f}}=?{f}∩ ?{f,?}} (Q(Π)) 1{{⊥,f}}= ?{f}∪ ?{⊥}=U({⊥,f}) 利用布爾剪枝方法，簡化后的廣義量詞的 tableau規(guī)則為 令 ?∈ L， i∈N ， 稱表達式 ?和 ?為正則公式 ， 其中 ={j|j∈N,j≥i} ， = {j| j∈N,j≤i} 。