摘  要： 针对命题逻辑的可判定性中真值表法复杂度高的问题，提出了一种基于命题逻辑联结符号完备性和与或树规则的命题逻辑的可判定性算法。算法首先利用常见的等价公式和与或树规则对命题逻辑的公式进行分解，然后参照分解后的树形结构将公式转换成范式形式，最后对照所得的判别式对命题逻辑公式进行判定。理论证明这种算法相比于具有指数级复杂度的真值表法效率高得多。
关键词： 命题逻辑；归纳定义；完备性；与或树；可判定性

    所谓命题逻辑的判定问题，即是否存在这样的算法，对于任意命题逻辑的公式，利用这个算法在有限步内判定是否是永真，是否是可满足的，是否是矛盾的[1]。命题逻辑的判定问题是一个已解决的问题。利用真值表法，对于有n个命题变元的公式，在不超过2n步内得出命题逻辑的判定问题，指数级的复杂度很难让人们接受。故命题逻辑的判定问题主要是考虑它的效率，在有限的范围内更快地解决这个问题。
1 命题逻辑基础
    命题逻辑是数理逻辑的一部分。在命题逻辑中，把简单命题作为基本单位；从简单命题出发，通过使用联结词来构成复合命题。命题逻辑的特征在于，在研究命题的逻辑形式时，只分析复合命题的逻辑形式，把复合命题分析到基本的命题成分即简单命题为止，而不去考虑简单命题自身的成分因素。简单命题被看作是一个整体，它是真的或假的。
1.1 命题逻辑语言￡
    命题逻辑语言￡是命题逻辑使用的形式语言，包含3类符号：第一类为命题符，如p、q、r表示任何命题符号；第二类包括5个联结符号：¬、∧、∨、→、⇔，它们依次表示非、合取、析取、蕴涵和等值于；第三类包括两个标点符号：“(”和“)”，它们依次称为左括号和右括号。



    (1)输入一个命题公式A；
    (2)若A为蕴涵形式，如A=B→C，则利用完备集对命题公式进行蕴涵释放，这个过程必须是递归的，因为B或C也可能是蕴涵；得到一个与公式A等价的命题公式A′；
    (3)命题公式A′利用德·摩根律和双重否定律将否定符号“?劭”移到各个命题变元之前，得到与A′等价的命题公式A″，显然A″的组成部分都是文字；
    (4)用分配律、结合律将命题公式化为合取范式或析取范式形式的公式A0，输出的A0与A是逻辑等值的。
    需要说明的是，此判定算法满足3个特性：(1)对于所有输入的命题公式，该算法是可以终止的，即算法具有可终止性；(2)对于每一个输入，调用该算法所得的输出是输入公式的一个等价公式；(3)所有由该算法计算的输出都是合取范式(CNF)或者析取范式(DNF)形式。

    同理可以得到，命题逻辑公式是矛盾的当且仅当它的析取范式中的每一个因子至少含有一个互补对。
    由于算法只涉及到对公式进行等值代换，其主要的时间消耗是在命题公式的范式求解过程中，故其复杂度大致为与或树的深度h。假设在公式A中出现原子命题的数目为n，最理想的状态是利用与或树规则分解完后形成一个满二叉树，最后一层为n个原子命题或者原子命题的否定，这样得到二叉树的层数为Llgn」+1，算法的复杂度下界大致为Llgn」+1；最坏的情况为，公式A中出现的是n个均不同的原子命题，这样只能通过真值表法去判定其为永真式或矛盾式，其算法复杂度为2n。显然，相比于真值表法的指数级复杂度，该算法的复杂度有所降低,提高了在判定过程中的效率。
    命题逻辑的判定问题是已解决的问题，但是本文对命题逻辑公式先进行等值替换构造互补对来进行判定的算法思路，对设计命题逻辑公式判定的推理机提供了理论基础[6]，同时对一阶谓词逻辑片段（如二元一阶谓词逻辑FO2）的可判定性证明有启发意义。
参考文献
[1] 张会凌.命题逻辑判定系统中基本真值矩阵的生成算法[J].甘肃联合大学学报，2005，19(1)：16-19.
[2] 陆钟万.面向计算机科学的数理逻辑[M].北京：科学出版社，2002.
[3] 屈婉玲，耿素云.离散数学[M].北京：高等教育出版社，2008.
[4] HUTH M，RYAN M.面向计算机科学的数理逻辑系统建模与推理[M].何伟，樊磊，译.北京：机械工业出版社，2007.
[5] NILSSON N J.人工智能[M].郑扣根，译.北京：机械工业出版社，2007.
[6] 郭远华.启发式方法生成命题逻辑可读证明[J].计算机应用研究，2011，28(12)：4429-4432.