楊杰

（山西職業(yè)技術學院，山西 太原030006）

經(jīng)典數(shù)理邏輯作為數(shù)學研究的重要分支，在以數(shù)理邏輯為主的證明理論中，一階邏輯語言成為其實現(xiàn)和證明的重要媒介，因此語言的可靠性和完整性成為邏輯證明的重要評估對象。本文基于經(jīng)典數(shù)理以及相關證明理論來進行一階自由變元tableau 實現(xiàn)過程分析。據(jù)文獻目前自動證明（ATP）仍是邏輯證明和推理研究的主要方法，其實現(xiàn)過程基本依賴于歸結法和語義Tableau 方法。

因此本文基于M.C.Fitting 研究基礎通過改進對應的算法，來進行算法的正確性評估，最后基于實驗基礎上，通過對比研究，進一步證明改進后的系統(tǒng)算法在推理效率和時間上均優(yōu)于常規(guī)算法[1-2]。

1 一階邏輯概述

目前，我們熟知的程序設計語言有C 語言、Java 等，這些語言以編程的形式，將語言和程序進行融合來對某個行業(yè)、領域進行表達和描述，例如在數(shù)學知識表現(xiàn)方面，一般的數(shù)學公式、定理以及推理都需要借助一階邏輯來進行知識的體現(xiàn)和表達，但一般情況下每個性質(zhì)、定理往往會有不同的性質(zhì)表達，因此在實際應用中會根據(jù)其適用范圍來進行語言的選擇。

例如在數(shù)學定理證明方面，往往需要一個一般意義的符號來表示內(nèi)在語言，如需要深入討論內(nèi)在語言，則需要再繼續(xù)增加一個元符號來進行語言的表達。因此在考慮語言性質(zhì)和用途方面，基本對所有的語言都適用，一般語言一般由邏輯符號和知識符號構成[3-4]。

2 一階邏輯的語義Tableau 方法

目前對于一階邏輯證明的方式多種多樣，一般情況有歸結法和語言Tableau 法可以適用，在語義Tableau 系統(tǒng)中，歸結法和語義Tableau 法都具有互制性，如要對假設A 進行證明，則需要提出假設A 的矛盾體，在假設過程中來對A 進行證明拓展、驗算，其拓展和驗算的方式一般是通過樹的形式來進行表達，每個節(jié)點都是公式。

Tableau 方法就是在樹的基礎上把樹的分支看成公式的假設之一，通過的公式類型可分為ɑ 公式、β 公式、否定公式、λ公式和δ 公式。每種公式相對應的語義Tableau 擴展規(guī)則如表1 所示：

表1 Tableau 擴展規(guī)則

根據(jù)以上Tableau 演變方式，因此對Tableau 概念進行多種定義。

3 一階自由語義Tableau 系統(tǒng)實現(xiàn)與改進

3.1 Tableau 系統(tǒng)實現(xiàn)

目前大部分的定理證明自動化都會根據(jù)語言歸結系統(tǒng)來完成，也有一部分是通過Tableau 系統(tǒng)來完成，尤其是隨著智能化技術的發(fā)展，根據(jù)語義Tableau 進行定理、假設的證明已經(jīng)成為趨勢。本文借助一階自由變元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），

3.2 Tableau 系統(tǒng)改進

為了對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。

4 實驗對比分析

本文基于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)化的必要性。

5 結論

由于目前一階邏輯自動定理存在一定的缺陷，為有效杜絕由于其缺陷而造成系統(tǒng)運行過程故障。本文邏輯證明和推理研究的研究方法，通過優(yōu)化改進對應的算法機制，來提高一階邏輯自動定理的效能和準確度，通過研究表明，優(yōu)化后的算法在比原有算法運行效率提高了88%且系統(tǒng)具有較強的兼容性，因此可被擴展到非經(jīng)典邏輯中，可以使此方法應用到不同領域中，從而提高了系統(tǒng)的應用范圍。