【正文】 ∈B i,并且Fiσ i＝ Giσ i 。 例： { (?x)((g(x) ≈ f(x))∨ ?(x≈ a))， (?x)(g(f(x)) ≈ x)， b≈ c， P(g(g(a)),b)， ?P(a,c)} ⑴ (?x)((g(x) ≈f(x))∨ ?(x≈a)) ⑵ (?x)(g(f(x)) ≈x) ⑶ b≈c ⑷ P(g(g(a)),b) ⑸ ?P(a,c) ⑹ g(f(x1)) ≈x1 ⑺ (g(x2) ≈f(x2))∨ ?(x2≈a) ⑻ (g(x2) ≈f(x2) ⑼ ?(x2≈a) ⑽ P(g(f(a)),b) ＊ ⑾ P(a,b) ⑿ P(a,c) ＊ 如果等式⑻應用到⑷的過程中， {g(a)/x2}代替 {a/x2} 將產(chǎn)生錯誤的方法，即 ⑽ * P(f(g(a)),b)代替 ⑽ P(g(f(a)),b) 那么 tableau不能封閉。 用 Visual Prolog語言在 Windows環(huán)境下進行了系統(tǒng) UniTAP的實現(xiàn)，程序中將識別出的 ?變量保存在一個表中，可以對表中的變量進行實例化，使分枝中的實例互不影響。這就導致了在推理過程中，產(chǎn)生大量的無關公式 Reeves方法 （ 1）含等詞的 tableau方法分析 P(s1, … ,sn) ?P(t1, … ,tn ) ? (s1≈t1) … ? (sn≈tn) ? (s1≈t1) … ? (sn≈tn) Reeves含等詞擴展規(guī)則 ?f(s1, … ,sn)≈f(t1, … ,tn) 優(yōu)點： 對封閉分枝的搜索更直接 存在問題： 如果一個分枝包含幾個等式和不等式，新的擴展規(guī)則也可能被看成同樣的等式和不等式來擴展，這樣連續(xù)不斷的新的擴展分枝被加入到 tableau中。] (? [s])μ (? [s])μ 含等詞自由變量 tableau擴展規(guī)則 μ 是 t和 t180。 一個替換 ?為等式合一問題的解當且僅當E?╞(s ?≈t ?)成立 。 第二階段是處理等詞 ，通過適當?shù)氖侄?， 限制等詞的使用 ， 以避免無關公式的產(chǎn)生 。 可靠性： 如果 T是 T2封閉的，那么公式 ?是不可滿足的。 ① 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ù)必須提高。 第一階段是在處理等詞之前 ， 應用 tableau擴展規(guī)則 ，將所有的 tableau擴展完成 ， 在這個過程中要求對 ?規(guī)則應用次數(shù)進行限制 。 (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ī)則 ， 并給出了可靠性和完備性的證明 。 在多值邏輯中 例： 在一階三值 Kleene邏輯中，可以對{0}(?x)?(x)進行擴展，其中 (Q(?))1({0})= {{0},{0, },{0,1},{0, ,1}}。 ⑵ 如果 (Q(?))1(S)=D(I)，則 S(?x)?(x)是可滿足的當且僅當對于所有的基項 t， I?(t)是可滿足的。 在效率和實現(xiàn)上都有較大的提高 時間效率 空間效率 Zabel方法 O(nk) O(n*k) 布爾剪枝方法 O(n*k) O(n) 例：考慮真值集合 FOUR={⊥ ,f,t,?}，定義量詞 Π ， Q(Π )= ，這里 為格中的交操作。 ⑷ 對于任何 i∈N 和分配格 L: (Q－１ (Π))( ?i)=U(?m)，其中 Mi是 MI(L)∩ ?i中的最小元素。 ⑻ 對于任何 i∈N 和分配格 L: (Q－１ (Σ))({i})=(U( ?j))∩(D( ?i)∪{ ?})，其中 Ji是 JI(L)∩ ?i中的最小元素。 {⊥}(Π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} 。 ⑽ 對于任何 i∈N ： (Q－１ (Σ))( ?i)=D(?i)。 ⑹ 如果 i∈JI(L) ，那么 (Q－１ (Σ))({i})=U({i})∩(D( ?i)∪{ ?})。 ⑵ 如果 L是分配格并且 i∈MI(L) ，那么 (Q－１ (Π))( ?i)=U(?i)。這一結(jié)論也是與經(jīng)典情況一致的。 定義 I，??I?N， 產(chǎn)生的關于布爾集格 2N的集合的下集為D(I)={X ?X?N,??X?I}。 提出了布爾剪枝方法 ， 將帶符號的公式與集合的上集／下集聯(lián)系起來 ， 使含量詞的一階公式的擴展規(guī)則大大簡化 。 （ 5）小 結(jié) 一是 二是 將計算等價類的結(jié)果以樹的結(jié)構(gòu)進行存儲 ， 利用樹的特點 ， 進行搜索的優(yōu)化 ， 提高推理效率 。 （ 3）如果使用 Jeffrey方法證明同一公式為重言式，等式規(guī)則的應用次數(shù)依賴于使用等式的次序，最好的情況下只需要 2個分枝即封閉，然而在較差的情況下可以產(chǎn)生幾百個分枝。 例 ： 證明公式 設未封閉分枝為 B， B轉(zhuǎn)換成集合 E(B)和 P(B)。 從第二階段開始只需要考慮等式 、 不等式以及潛在的封閉原子對 ， 這樣使含等詞的 tableau在一個更適合的數(shù)據(jù)結(jié)構(gòu) P(B)和 E(B)下進行 。 ⑵ 對于 B上的潛在封閉原子對 p(s1, … ,sn)和 ?p(t1, … ,tn)(這里 p≠≈) ， 存在某一替換 ， 使得 {s1?≠t 1?∨ ? ∨s n?≠t n?}?P(B)； 等式合一問題集合 將 tableau擴展分成兩個階段 。 在該方法中 ，將 tableau分成兩個階段 ， 等詞單獨處理 ， 通過提取等式合一問題并求解解替換封閉 tableau， 該方法進一步限制了 tableau的搜索空間 ， 提高了tableau的推理效率 。 Fitting方法 （ 1）含等詞的 tableau方法分析 t≈s s≈t ? [t180。 另外在非經(jīng)典邏輯中的識別 ?公式的方法與經(jīng)典邏輯類似 ，因此只要稍加修改就可將該方法擴展到非經(jīng)典邏輯中 。該方法很難用于機器實現(xiàn)，并且不可避免地產(chǎn)生回溯。 (?P(a)∨ ?P(b))∧(( ?x)P(x)) ?P(a)∨ ?P(b) (?x)P(x) P(y) ?P(a) ?P(b) P(y)被識別為 ?公式 ， 因此 P(y)不再需要實例化 ， 可立即封閉 。一旦一個公式被識為 ?公式，那么尋找一個封閉 tableau的替換 ?就變得比較容易：對于 ?公式中的變量不需要實例化。 限制的次數(shù)過多 ， 由于 ?規(guī)則使用次數(shù)的不確定性 ， 必然會導致大量的冗余推理產(chǎn)生 ， 使證明過程的搜索空間膨脹 。z?x 問題序號 ?規(guī)則 ?+規(guī)則 ?++規(guī)則 節(jié)點數(shù) (個 ) 時間 (毫秒 ) 節(jié)點數(shù) (個 ) 時間 (毫秒 ) 節(jié)點數(shù) (個 ) 時間 (毫秒 ) 1 30 140 30 140 18 85 2 41 168 36 150 36 150 3 26 87 26 87 26 87 4 75 201 75 201 53 160 5 180 304 89 210 60 154 6 49 170 34 130 34 130 7 104 280 104 280 58 170 8 33 150 33 150 20 100 9 27 135 27 135 27 135 10 87 209 87 209 46 140 可以看出 ， 從 tableau擴展節(jié)點數(shù)和封閉時間上進行了比較 ， 其中有 2個問題 ， 應用 ?+、 ?++規(guī)則沒有變化 ， 其中有 6個問題 ，應用 ?++規(guī)則后 ， 節(jié)點數(shù)和時間上都有較大幅度的減少 。 ⑵ (?x)P(x)∨( ?y)P(y) ⑺ P(g(x1)) ⑴ (?x)?P(x) ⑶ ?P(x1) ⑷ (?x)P(x) ⑸ (?y)P(y) ⑹ P(f(x1)) ⑻ ?P(x2) ⑼ ?P(x3) f(x1)/x2 g(x1)/x3 * * 應用 ? －規(guī)則 ⑸ (?y)P(y) ⑼ ?P(x3) ⑴ (?x)?P(x) ⑵ (?x)P(x)∨( ?y)P(y) ⑶ ?P(x1) ⑷ (?x)P(x) ⑹ P(c1) ⑻ ?P(x2) c1/x2 c2/x3 * * 應用 ? + －規(guī)則 ⑺ P(c2) ⑴ (?x)?P(x) ⑶ ?P(x1) ⑷ (?x)P(x) ⑸ (?y)P(y) ⑹ P(c) c/x1 * * ⑵ (?x)P(x)∨( ?y)P(y) 應用 ?++－規(guī)則 ?+＋ －規(guī)則為： ? ? (f[?](x1,… ,xn) f[?]是賦予 ?的函數(shù)符號，在等價類 [?]中所有公式賦予唯一的函數(shù)符號 f[?]?Σ 。 ? ?1(f(x1,… ,xn) f是一個新的 Skolem函數(shù)符號 ， x1,… ,xn是分枝中出現(xiàn)的自由變量 ? ?(f(x1,… ,xn) f是一個新的 Skolem函數(shù)符號 ， x1,… ,xn是出現(xiàn)在 ?中的自由變量 ． ? ?1(x) ?規(guī)則 ?+規(guī)則 ?+規(guī)則與 ?規(guī)則的區(qū)別是：在 ?