楊杰
(山西職業(yè)技術學院,山西 太原030006)
經典數(shù)理邏輯作為數(shù)學研究的重要分支,在以數(shù)理邏輯為主的證明理論中,一階邏輯語言成為其實現(xiàn)和證明的重要媒介,因此語言的可靠性和完整性成為邏輯證明的重要評估對象。本文基于經典數(shù)理以及相關證明理論來進行一階自由變元tableau 實現(xiàn)過程分析。據(jù)文獻目前自動證明(ATP)仍是邏輯證明和推理研究的主要方法,其實現(xiàn)過程基本依賴于歸結法和語義Tableau 方法。
因此本文基于M.C.Fitting 研究基礎通過改進對應的算法,來進行算法的正確性評估,最后基于實驗基礎上,通過對比研究,進一步證明改進后的系統(tǒng)算法在推理效率和時間上均優(yōu)于常規(guī)算法[1-2]。
目前,我們熟知的程序設計語言有C 語言、Java 等,這些語言以編程的形式,將語言和程序進行融合來對某個行業(yè)、領域進行表達和描述,例如在數(shù)學知識表現(xiàn)方面,一般的數(shù)學公式、定理以及推理都需要借助一階邏輯來進行知識的體現(xiàn)和表達,但一般情況下每個性質、定理往往會有不同的性質表達,因此在實際應用中會根據(jù)其適用范圍來進行語言的選擇。
例如在數(shù)學定理證明方面,往往需要一個一般意義的符號來表示內在語言,如需要深入討論內在語言,則需要再繼續(xù)增加一個元符號來進行語言的表達。因此在考慮語言性質和用途方面,基本對所有的語言都適用,一般語言一般由邏輯符號和知識符號構成[3-4]。
目前對于一階邏輯證明的方式多種多樣,一般情況有歸結法和語言Tableau 法可以適用,在語義Tableau 系統(tǒng)中,歸結法和語義Tableau 法都具有互制性,如要對假設A 進行證明,則需要提出假設A 的矛盾體,在假設過程中來對A 進行證明拓展、驗算,其拓展和驗算的方式一般是通過樹的形式來進行表達,每個節(jié)點都是公式。
Tableau 方法就是在樹的基礎上把樹的分支看成公式的假設之一,通過的公式類型可分為ɑ 公式、β 公式、否定公式、λ公式和δ 公式。每種公式相對應的語義Tableau 擴展規(guī)則如表1 所示:
表1 Tableau 擴展規(guī)則
根據(jù)以上Tableau 演變方式,因此對Tableau 概念進行多種定義。
目前大部分的定理證明自動化都會根據(jù)語言歸結系統(tǒng)來完成,也有一部分是通過Tableau 系統(tǒng)來完成,尤其是隨著智能化技術的發(fā)展,根據(jù)語義Tableau 進行定理、假設的證明已經成為趨勢。本文借助一階自由變元Tableau 系統(tǒng)來進行假設命題等相關的證明,但在運行過程中往往需要額外增加一些限制條件,來進行語言系統(tǒng)的拓展運算。本文就主要步驟來進行具體說明[5-6]:
一階自由變元Tableau 的實現(xiàn)代碼的實現(xiàn):
目前一階自由變元Tableau 的實現(xiàn)主要借助remove(_,_,_)等命題來進行邏輯表達,如具體的代碼如下:
remove(X,[],[]).
remove(X,[Y|Tail],Newtail):-
X==Y,remove(X,Tail,Newtail).
remove(X,[Y|Tail],[Y|Newtail]):-
X==Y,remove(X,Tail,Newtail).
每個運行規(guī)則都需要特定的符號來進行表達,如本文通過函數(shù)符號f(n)來進行函數(shù)符號的表達,n 為正整數(shù),每個規(guī)則的n 會增加1 個單元,本文引用符號funcount 來進行函數(shù)n 值的標記。程序引入謂語符號reset 來進行n 值的復原,具體實現(xiàn)代碼如下所示:
funcount(1).newfuncount(N):-funcount(N),
為了對Tableau 系統(tǒng)改進,本文通過分析一階自由語義Tableau 系統(tǒng)實現(xiàn)發(fā)現(xiàn),在語言分支過程中,彼此之間的分支是封閉的,但在對應的謂語詞驗證中,系統(tǒng)又會對每個Tableau 分支進行檢測識別,因此造成效率的降低和重復檢測;為了進一步提高程序檢測效率,本文基于M.C.Fitting 來對Tableau 進行改良優(yōu)化,實現(xiàn)對互補程序的單一檢測,提高系統(tǒng)分支的檢測效率、降低算法的運行空間[7]。
算法TabProver(X)
輸入一階邏輯公式X、
輸出如果X 成立,則輸入yes,否則no
定理:假設A 為公式、如果A 不是檢測對象,則算法結束且結束終止于no;否則,算法止于yes。
證明:假設算法是可以被終止的,設T 為集合中的公式且未被實例化,每個運行后,分支中的T 個數(shù)會減少,因為X 是有限的,所以循環(huán)會被終止,則該算法結束,假設算法是正確的,那么假設A 不是有效的,但最終止于yes;因此根據(jù)循環(huán)條件假設A 是有效的,和原假設矛盾,但由于系統(tǒng)止于no,當A 是有效的,但不止于yes,則公式被拓展后,Tableau 分支沒有封閉,則A不是有效的,和原假設矛盾,因此算法止于yes。
本文基于Prolog 語言在Windows 下,以一階自由語義Tableau 系統(tǒng)分別對改進的系統(tǒng)進行典型問題驗證并進行對比分析。
通過實驗得出改進優(yōu)化前的證明該定理所消耗的時間為0.122s,改進優(yōu)化后所需要的時間為0.015s,運行效率也提高了90%,以同樣的方式對10 個問題進行實驗,具體結果如表2 和圖1 所示。
表2 改進前后時間記錄表
圖1 改進前后時間效果對比
從以上圖表可以看出,10 個問題運行效率都顯著提高,最為表現(xiàn)突出的為問題1、3、4、7、10 等。進一步可得出結論為優(yōu)化后的系統(tǒng)耗能時間減少了90%,因此改進后的系統(tǒng)TabProver與原系統(tǒng)相比較在運行效率顯著提升,證明系統(tǒng)算法優(yōu)化的必要性。
由于目前一階邏輯自動定理存在一定的缺陷,為有效杜絕由于其缺陷而造成系統(tǒng)運行過程故障。本文邏輯證明和推理研究的研究方法,通過優(yōu)化改進對應的算法機制,來提高一階邏輯自動定理的效能和準確度,通過研究表明,優(yōu)化后的算法在比原有算法運行效率提高了88%且系統(tǒng)具有較強的兼容性,因此可被擴展到非經典邏輯中,可以使此方法應用到不同領域中,從而提高了系統(tǒng)的應用范圍。