一階自由變元tableau 實現過程分析

楊杰

（山西職業技術學院，山西 太原030006）

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

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

1 一階邏輯概述

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

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

2 一階邏輯的語義Tableau 方法

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

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

表1 Tableau 擴展規則

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

3 一階自由語義Tableau 系統實現與改進

3.1 Tableau 系統實現

目前大部分的定理證明自動化都會根據語言歸結系統來完成，也有一部分是通過Tableau 系統來完成，尤其是隨著智能化技術的發展，根據語義Tableau 進行定理、假設的證明已經成為趨勢。本文借助一階自由變元Tableau 系統來進行假設命題等相關的證明，但在運行過程中往往需要額外增加一些限制條件，來進行語言系統的拓展運算。本文就主要步驟來進行具體說明[5-6]：

一階自由變元Tableau 的實現代碼的實現：

目前一階自由變元Tableau 的實現主要借助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）.

每個運行規則都需要特定的符號來進行表達，如本文通過函數符號f（n）來進行函數符號的表達，n 為正整數，每個規則的n 會增加1 個單元，本文引用符號funcount 來進行函數n 值的標記。程序引入謂語符號reset 來進行n 值的復原，具體實現代碼如下所示：

funcount（1）.newfuncount（N）:-funcount（N），

3.2 Tableau 系統改進

為了對Tableau 系統改進，本文通過分析一階自由語義Tableau 系統實現發現，在語言分支過程中，彼此之間的分支是封閉的，但在對應的謂語詞驗證中，系統又會對每個Tableau 分支進行檢測識別，因此造成效率的降低和重復檢測；為了進一步提高程序檢測效率，本文基于M.C.Fitting 來對Tableau 進行改良優化，實現對互補程序的單一檢測，提高系統分支的檢測效率、降低算法的運行空間[7]。

算法TabProver（X）

輸入一階邏輯公式X、

輸出如果X 成立，則輸入yes，否則no

定理：假設A 為公式、如果A 不是檢測對象，則算法結束且結束終止于no；否則，算法止于yes。

證明：假設算法是可以被終止的，設T 為集合中的公式且未被實例化，每個運行后，分支中的T 個數會減少，因為X 是有限的，所以循環會被終止，則該算法結束，假設算法是正確的，那么假設A 不是有效的，但最終止于yes；因此根據循環條件假設A 是有效的，和原假設矛盾，但由于系統止于no，當A 是有效的，但不止于yes，則公式被拓展后，Tableau 分支沒有封閉，則A不是有效的，和原假設矛盾，因此算法止于yes。

4 實驗對比分析

本文基于Prolog 語言在Windows 下，以一階自由語義Tableau 系統分別對改進的系統進行典型問題驗證并進行對比分析。

通過實驗得出改進優化前的證明該定理所消耗的時間為0.122s，改進優化后所需要的時間為0.015s，運行效率也提高了90%，以同樣的方式對10 個問題進行實驗，具體結果如表2 和圖1 所示。

表2 改進前后時間記錄表

圖1 改進前后時間效果對比

從以上圖表可以看出，10 個問題運行效率都顯著提高，最為表現突出的為問題1、3、4、7、10 等。進一步可得出結論為優化后的系統耗能時間減少了90%，因此改進后的系統TabProver與原系統相比較在運行效率顯著提升，證明系統算法優化的必要性。

5 結論

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