語義Tableau定理證明器的Prolog實現

高華　江建國　蘇賀靚

【摘 要】語義Tableau是一種具有較強通用性和適用性的推理方法。基于Prolog語言，并利用語義Tableau方法，在M.C.Fitting提出的一階邏輯自動定理證明器的基礎上提出了一些改進，給出了改進后相應的算法，并且對算法的可終止性和正確性進行了證明。實驗結果表明，優化后的語義Tableau定理證明器，大大提高推理效率。

【關鍵詞】語義Tableau；定理證明器；Prolog

【Abstract】Semantic Tableau is a strong versatility and applicability of the method of reasoning. Basing on the Prolog language， and the use of Semantic Tableau method， it made some improvements which based on the first-order logic automated theorem proposed by M.C.Fitting， and gave the corresponding algorithm. In addition， it gives the proofs of its terminability and correctness. Experimental results shows that the optimized Semantic Tableau theorem prover makes the Tableau close early and improves greatly in time efficiency of deduction.

【Key words】Semantic tableau； Theorem prover； Prolog

0 引言

自動定理證明（Automated Theorem Proving， 簡稱ATP）一直是人工智能領域內的一個重大研究課題。在軟件生成，軟硬件驗證，推理數據庫等領域，自動定理證明都有著廣泛的應用。研究自動定理證明的方法有很多，常見的自動定理證明的方法有兩類：歸結法和語義Tableau方法。有關這兩種方法的應用有很多，例如許偉濤和張家鋒等人都將歸結法應用在格值邏輯上，并取得了重大的突破[1-2]；劉全，孫吉貴根據語義Tableau方法提出了一種新的定理證明器TableauTAP[3]。

語義Tableau是在20世紀50年代由Beth和Hintikka發明的，之后由Sumullan和Fitting進一步完善。自語義Tableau問世以來，對語義Tableau自動定理證明器的探索一直吸引著廣大人工智能研究者。很多文獻在該方面進行了探索。

B.Becke和J.Posegga提出了一種高效、簡潔、安全的一階邏輯定理證明器leanTAP[4-5]。leanTAP系統是由五條Prolog語句構成的。由于該系統本質上利用了Prolog的搜索機制，因此用不同的語言書寫該程序時，我們至少要模仿Prolog的一部分。由于程序的短小，B.Becke和J.Posegga能夠對該系統的完備性和可靠性的證明做一個簡述。但是其完備性證明的具體過程卻相對復雜。

為了簡化系統完備性的證明以及使leanTAP更容易被理解，M.C.Fitting從leanTAP中提取出了一種新的序列演算[6]。該序列演算即使在沒有所有結構規則的情況下，仍具有可靠性和完備性。而且還很容易被擴展到其他的邏輯中去。

M.C.Fitting提出了另一種Tableau的一階邏輯自動定理證明器系統[7]。該系統是在Windows環境下，應用Prolog語言實現的。其相應的可靠性和完備性的證明是采用模型存在定理來完成的。該系統的方法易于擴展，且具有很強的通用性，這使得它能夠很快的被大多數人接受。只是在實現效率問題上還存在著一些不足。應用M.C.Fitting的Tableau系統相應的擴展規則，我們可以構造出一個含有n個分枝的Tableau分枝樹，且該分枝樹上的n-1個分枝是封閉的。然而在使用謂詞closed對其進行驗證時，系統又一次對整個Tableau分枝樹進行了檢測，這是沒有必要的。

在M.C.Fitting工作的基礎上，針對以上問題，本文對其算法做了相應的改進，并對改進后的算法進行了可終止性和正確性的證明。將改進后的系統與改進前的系統進行對比，結果表明，改進后的系統在推理的時間效率和空間效率上都有很大的提高。

2 Tableau算法

本文給出的Tableau算法是在M.C.Fitting的基礎上作了進一步的改進而得出的。一方面，為防止對某分枝中已經互補的子式[8]繼續擴展。系統在每次擴展之后，應立即對其封閉性做出檢驗，而不是等把整個Tableau分枝樹都擴展完，再驗證它是否為封閉的。另一方面，已經封閉的分枝，應把它去掉。否則，系統會又一次地對其進行擴展。這增加了算法的復雜度，從而導致了系統實現效率降低。

定理1 設X為公式，若X不是有效的，則算法終止，且最后終止于No；否則，算法終止于Yes。

證明：首先，該算法是可以終止的。設T為[〈X〉]中非原子公式或者是未實例化的量詞公式的集合，每次循環之后，T的個數就會減少1，由于X是有限的，所以循環必將終止，即該算法終止；其次，該算法也是正確的。假設X不是有效的，但最后終止于Yes，則由循環的條件可知，該分枝樹中沒有其他任何分枝，即該分枝樹中的所有分枝都被刪去了，進而該分枝樹的所有分枝都是閉的。由定義2可知，此時的Tableau是閉的，所以X有一個Tableau證明。由文獻[7]中自由語義變量Tableau的可靠性可知，X是有效的。這與假設矛盾，因此系統終止于No。若X是有效的，但不以Yes終止，由算法可知，在對所有的公式都進行擴展之后，Tableau樹仍是不封閉的，因此X不是有效的，這與假設矛盾。因此算法終止于Yes。

3 Prolog實現

把一個Tableau分枝樹看作是由它上分枝構成的一個列表T=[B1，B2，…，Bn]，列表中的每個元素Bi代表一個分枝，且每個分枝Bi也都可以寫成由該分枝上所有公式構成的一個列表B=[φ1，φ2，…，φn]列表中的每個元素φi表示一個公式。若Tableau分枝樹的其中的一個分枝Bi是閉的，則把此分枝從列表T中刪去。最后，如果構成的Tableau分枝樹的列表T為空，則有該Tableau是閉的。

由于本文構造的Tableau是嚴格的，因此，用Tableau擴展規則作用后的公式應從列表中刪去，從而使得由每個分枝構成的列表中的元素為原子或未擴展的公式。

相對于文獻[7]，本文在驗證分枝閉的過程中增加了對分枝閉的檢驗，來防止對已封閉了的分枝繼續使用Tableau擴展規則進行擴展。

為證明公式X的有效性，本文將證明器的開始目標設置為：test（X，Qdepth）。X是待擴展的原公式；Qdepth是γ規則使用的次數。當Qdepth達到最大值時，程序將不再被執行。因為擴展規則中的γ規則要求從γ到γ（t），所以限制γ規則的使用次數是很有必要的。這里t是任意的閉項。由于閉項t的個數是無窮的，因此γ規則會無休止地執行下去。

程序中對公式的擴展是用謂詞expand（Tree，Qdepth，Newtree）來實現的。這里，Tree是待擴展的語義分枝樹；Qdepth用來限制γ規則的使用次數；Newtree是擴展之后得到的新的Tableau分枝樹。對Tableau分枝的擴展是采取遞歸的方式進行的。擴展的實際操作過程如下：

Singlestep（OldTableau，OldQdepth，NewTableau，NewQdepth）

這里OldTableau，NewTableau分別是待擴展的分枝樹和擴展完之后的分枝樹；OldQdepth與NewQdepth分別是擴展前后Qdepth的值。

4 對比實驗

改進后的系統是在Windows環境下，應用SWI-Prolog語言實現的。使用改進后的系統對文獻[9]中的10個問題進行證明，并與改進前的系統作比較，結果見表2。

由表1可以得出，改進后的系統TabProver與原系統相比較在運行時間效率方面有了很大的提高，從而本文對原系統的改進是可行有效的。

5 結語

對于自動推理而言，考察其推理效率的一個重要指標是推理所用的時間和空間。近年來隨著人工智能技術的進一步發展，自動推理在效率方面的要求也越來越高，基于語義Tableau的推理系統也存在效率方面的問題。本文在M.C.Fitting的基礎上針對分枝閉檢驗的效率問題提出了相應的改進。改進后的系統，一方面增加了封閉性的檢驗；另一方面對已經封閉的分枝采取立即刪除。此外，本文還給出了改進后的算法，證明了算法的正確性與可終止性，并在Windows環境下對系統進行了實現。實驗結果表明，改進后系統的推理復雜度大大降低了。

原有的一階邏輯自動定理器由于涉及對量詞的處理，因此導致了該證明器的運行效率相對較低，這給人們帶來了不便。今后將要進行的工作是：通過引入斯科拉姆化方法消去公式中的存在量詞，并驗證是否可以提高相應的效率。此外，由于語義Tableau方法具有較強的通用性，因此可以嘗試將其擴展到非經典邏輯中，從而達到該方法在不同領域的應用。

【參考文獻】

[1]XU Wei-tao ZHANG Wen-qiang ZHANG De-xian et al. α-generalized resolution principle based on the lattice-valued first-order logic system[J]. Journal of XiDian University，2014， 41（1）：135-139.許偉濤，張聞強，張德賢，等.格值一階邏輯系統的α廣義歸結原理[J].西安電子科技大學學報，2014，41（1）：135-139.

[2]ZAHNG Jia-feng， XU Yang. α-semantic resolution method based on lattice-valued first-order logic LF（X）[J]. Computer Science， 2014， 41（9）：274-279.張家鋒， 徐揚. 格值一階邏輯LF（X）中的α-語義歸結方法[J]. 計算機科學，2014，41（9）：274-278.

[3]LIU Guan， SUN Ji-gui. Theorem proving system based on tableau-tableauTAP[J]. Computer Engineering， 2006， 32（7）：38-46.劉全，孫吉貴. 基于Tableau的定理機器證明系統TableauTAP[J].計算機工程， 2006，32（7）：38-46.

[4]B BECKERT， J POSEGGA， LEANTAP. Lean tableau-based deduction[J]. Journal of Automated Reasoning， 1995，15（3）：339-358.

[5]B BECKERT， J POSEGGA. Logic programming as a basis for automated deduction[J]. The Journal of Logic Programming， 1996，28（3）：231-236.

[6]M FITTING. LeanTAP revisited[J]. Journal of Logic and Computation， 1998， 8（1）：33-47.

[7]M C FITTING. First-order logic and automated theorem proving[M]. 2rd ed. Springer-Verlag， 1996.

[8]LIU Guan， SUN Ji-gui， YU Wan-jun. An improved method of δ-rule in free variable semantic tableau[J]. Journal of Computer Research And Development， 2004，41（7）：1068-1073. 劉全，孫吉貴，于萬鈞.自由變量語義Tableau中δ規則的一種改進方法[J].計算機研究與發展，2004，41（7）：1068-1073.

[9]F J PELLETIER. Seventy-five Problems for testing automatic theorem provers[J]. Journal of Automated Reasoning， 1986，2：191-216.

[責任編輯：湯靜]