命题公式的一种演绎判定方法

A Deduction-Based Decision Method of Propositional Formulas

目前命题公式的判定方法大都是基于语义的,不能给出演绎过程,而演绎过程是许多推理性应用的重要依据.文中针对命题演算系统L,提出了一种可同时给出演绎过程的判定方法——演绎判定方法.首先定义了消解复杂性的两种范式:最简范式和文字范式,在此基础上采用演绎方法证明了L中的可判定性定理,并设计了命题公式的演绎判定算法P(F).P(F)的时间复杂度为O(n3),远远小于基于真值表法的O(2n)和基于策略方案HAL的O(n5).

As most of the present decision methods of propositional formulas are based on semantics and cannot give an important reference in many reasoning applications, namely deduction procedure, a deduction-based decision method that can give the deduction procedure during the decision procedure is presented based on the propositional calculus system L. Two normal forms, namely the simplest normal form and the literal one, are defined to overcome the complexity of formula decision. Based on the two normal forms, the decidability theorem in L is then proved and a deduction-based decision algorithm P（F） is designed. The time complexity O（ n^3） of P（F） is much less than the complexityO （ 2n ） of the true value table method and the complexity O（ n^5 ） of HAL based on the tactic scheme.