高華　江建國　蘇賀靚

【摘 要】語義Tableau是一種具有較強(qiáng)通用性和適用性的推理方法?；赑rolog語言，并利用語義Tableau方法，在M.C.Fitting提出的一階邏輯自動(dòng)定理證明器的基礎(chǔ)上提出了一些改進(jìn)，給出了改進(jìn)后相應(yīng)的算法，并且對算法的可終止性和正確性進(jìn)行了證明。實(shí)驗(yàn)結(jié)果表明，優(yōu)化后的語義Tableau定理證明器，大大提高推理效率。

【關(guān)鍵詞】語義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 引言

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

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

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

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

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

在M.C.Fitting工作的基礎(chǔ)上，針對以上問題，本文對其算法做了相應(yīng)的改進(jìn)，并對改進(jìn)后的算法進(jìn)行了可終止性和正確性的證明。將改進(jìn)后的系統(tǒng)與改進(jìn)前的系統(tǒng)進(jìn)行對比，結(jié)果表明，改進(jìn)后的系統(tǒng)在推理的時(shí)間效率和空間效率上都有很大的提高。

2 Tableau算法

本文給出的Tableau算法是在M.C.Fitting的基礎(chǔ)上作了進(jìn)一步的改進(jìn)而得出的。一方面，為防止對某分枝中已經(jīng)互補(bǔ)的子式[8]繼續(xù)擴(kuò)展。系統(tǒng)在每次擴(kuò)展之后，應(yīng)立即對其封閉性做出檢驗(yàn)，而不是等把整個(gè)Tableau分枝樹都擴(kuò)展完，再驗(yàn)證它是否為封閉的。另一方面，已經(jīng)封閉的分枝，應(yīng)把它去掉。否則，系統(tǒng)會(huì)又一次地對其進(jìn)行擴(kuò)展。這增加了算法的復(fù)雜度，從而導(dǎo)致了系統(tǒng)實(shí)現(xiàn)效率降低。

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

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

3 Prolog實(shí)現(xiàn)

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

由于本文構(gòu)造的Tableau是嚴(yán)格的，因此，用Tableau擴(kuò)展規(guī)則作用后的公式應(yīng)從列表中刪去，從而使得由每個(gè)分枝構(gòu)成的列表中的元素為原子或未擴(kuò)展的公式。

相對于文獻(xiàn)[7]，本文在驗(yàn)證分枝閉的過程中增加了對分枝閉的檢驗(yàn)，來防止對已封閉了的分枝繼續(xù)使用Tableau擴(kuò)展規(guī)則進(jìn)行擴(kuò)展。

為證明公式X的有效性，本文將證明器的開始目標(biāo)設(shè)置為：test（X，Qdepth）。X是待擴(kuò)展的原公式；Qdepth是γ規(guī)則使用的次數(shù)。當(dāng)Qdepth達(dá)到最大值時(shí)，程序?qū)⒉辉俦粓?zhí)行。因?yàn)閿U(kuò)展規(guī)則中的γ規(guī)則要求從γ到γ（t），所以限制γ規(guī)則的使用次數(shù)是很有必要的。這里t是任意的閉項(xiàng)。由于閉項(xiàng)t的個(gè)數(shù)是無窮的，因此γ規(guī)則會(huì)無休止地執(zhí)行下去。

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

Singlestep（OldTableau，OldQdepth，NewTableau，NewQdepth）

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

4 對比實(shí)驗(yàn)

改進(jìn)后的系統(tǒng)是在Windows環(huán)境下，應(yīng)用SWI-Prolog語言實(shí)現(xiàn)的。使用改進(jìn)后的系統(tǒng)對文獻(xiàn)[9]中的10個(gè)問題進(jìn)行證明，并與改進(jìn)前的系統(tǒng)作比較，結(jié)果見表2。

由表1可以得出，改進(jìn)后的系統(tǒng)TabProver與原系統(tǒng)相比較在運(yùn)行時(shí)間效率方面有了很大的提高，從而本文對原系統(tǒng)的改進(jìn)是可行有效的。

5 結(jié)語

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

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

【參考文獻(xiàn)】

[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.許偉濤，張聞強(qiáng)，張德賢，等.格值一階邏輯系統(tǒng)的α廣義歸結(jié)原理[J].西安電子科技大學(xué)學(xué)報(bào)，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.張家鋒， 徐揚(yáng). 格值一階邏輯LF（X）中的α-語義歸結(jié)方法[J]. 計(jì)算機(jī)科學(xué)，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的定理機(jī)器證明系統(tǒng)TableauTAP[J].計(jì)算機(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中δ規(guī)則的一種改進(jìn)方法[J].計(jì)算機(jī)研究與發(fā)展，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.

[責(zé)任編輯：湯靜]