摘 要： 針對命題邏輯的可判定性中真值表法復(fù)雜度高的問題，提出了一種基于命題邏輯聯(lián)結(jié)符號完備性和與或樹規(guī)則的命題邏輯的可判定性算法。算法首先利用常見的等價公式和與或樹規(guī)則對命題邏輯的公式進行分解，然后參照分解后的樹形結(jié)構(gòu)將公式轉(zhuǎn)換成范式形式，最后對照所得的判別式對命題邏輯公式進行判定。理論證明這種算法相比于具有指數(shù)級復(fù)雜度的真值表法效率高得多。
關(guān)鍵詞： 命題邏輯；歸納定義；完備性；與或樹；可判定性
所謂命題邏輯的判定問題，即是否存在這樣的算法，對于任意命題邏輯的公式，利用這個算法在有限步內(nèi)判定是否是永真，是否是可滿足的，是否是矛盾的[1]。命題邏輯的判定問題是一個已解決的問題。利用真值表法，對于有n個命題變元的公式，在不超過2n步內(nèi)得出命題邏輯的判定問題，指數(shù)級的復(fù)雜度很難讓人們接受。故命題邏輯的判定問題主要是考慮它的效率，在有限的范圍內(nèi)更快地解決這個問題。
1 命題邏輯基礎(chǔ)
命題邏輯是數(shù)理邏輯的一部分。在命題邏輯中，把簡單命題作為基本單位；從簡單命題出發(fā)，通過使用聯(lián)結(jié)詞來構(gòu)成復(fù)合命題。命題邏輯的特征在于，在研究命題的邏輯形式時，只分析復(fù)合命題的邏輯形式，把復(fù)合命題分析到基本的命題成分即簡單命題為止，而不去考慮簡單命題自身的成分因素。簡單命題被看作是一個整體，它是真的或假的。
1.1 命題邏輯語言￡
命題邏輯語言￡是命題邏輯使用的形式語言，包含3類符號：第一類為命題符，如p、q、r表示任何命題符號；第二類包括5個聯(lián)結(jié)符號：¬、∧、∨、→、⇔，它們依次表示非、合取、析取、蘊涵和等值于；第三類包括兩個標(biāo)點符號：“(”和“)”，它們依次稱為左括號和右括號。
(1)輸入一個命題公式A；
(2)若A為蘊涵形式，如A=B→C，則利用完備集對命題公式進行蘊涵釋放，這個過程必須是遞歸的，因為B或C也可能是蘊涵；得到一個與公式A等價的命題公式A′；
(3)命題公式A′利用德·摩根律和雙重否定律將否定符號“?劭”移到各個命題變元之前，得到與A′等價的命題公式A″，顯然A″的組成部分都是文字；
(4)用分配律、結(jié)合律將命題公式化為合取范式或析取范式形式的公式A0，輸出的A0與A是邏輯等值的。
需要說明的是，此判定算法滿足3個特性：(1)對于所有輸入的命題公式，該算法是可以終止的，即算法具有可終止性；(2)對于每一個輸入，調(diào)用該算法所得的輸出是輸入公式的一個等價公式；(3)所有由該算法計算的輸出都是合取范式(CNF)或者析取范式(DNF)形式。
同理可以得到，命題邏輯公式是矛盾的當(dāng)且僅當(dāng)它的析取范式中的每一個因子至少含有一個互補對。
由于算法只涉及到對公式進行等值代換，其主要的時間消耗是在命題公式的范式求解過程中，故其復(fù)雜度大致為與或樹的深度h。假設(shè)在公式A中出現(xiàn)原子命題的數(shù)目為n，最理想的狀態(tài)是利用與或樹規(guī)則分解完后形成一個滿二叉樹，最后一層為n個原子命題或者原子命題的否定，這樣得到二叉樹的層數(shù)為Llgn」+1，算法的復(fù)雜度下界大致為Llgn」+1；最壞的情況為，公式A中出現(xiàn)的是n個均不同的原子命題，這樣只能通過真值表法去判定其為永真式或矛盾式，其算法復(fù)雜度為2n。顯然，相比于真值表法的指數(shù)級復(fù)雜度，該算法的復(fù)雜度有所降低,提高了在判定過程中的效率。
命題邏輯的判定問題是已解決的問題，但是本文對命題邏輯公式先進行等值替換構(gòu)造互補對來進行判定的算法思路，對設(shè)計命題邏輯公式判定的推理機提供了理論基礎(chǔ)[6]，同時對一階謂詞邏輯片段（如二元一階謂詞邏輯FO2）的可判定性證明有啟發(fā)意義。
參考文獻
[1] 張會凌.命題邏輯判定系統(tǒng)中基本真值矩陣的生成算法[J].甘肅聯(lián)合大學(xué)學(xué)報，2005，19(1)：16-19.
[2] 陸鐘萬.面向計算機科學(xué)的數(shù)理邏輯[M].北京：科學(xué)出版社，2002.
[3] 屈婉玲，耿素云.離散數(shù)學(xué)[M].北京：高等教育出版社，2008.
[4] HUTH M，RYAN M.面向計算機科學(xué)的數(shù)理邏輯系統(tǒng)建模與推理[M].何偉，樊磊，譯.北京：機械工業(yè)出版社，2007.
[5] NILSSON N J.人工智能[M].鄭扣根，譯.北京：機械工業(yè)出版社，2007.
[6] 郭遠華.啟發(fā)式方法生成命題邏輯可讀證明[J].計算機應(yīng)用研究，2011，28(12)：4429-4432.