Deduction-based decision method of propositional formulas

作者：Qi, De-Yu^*; Li, Xiao-Xin

来源：Journal of South China University of Technology(Natural Science Edition), 2008, 36(9): 71-76.

• Automatic theorem proving
• Decision procedure
• Deduction-based decision
• Formula decision
• Propositional calculus
• Propositional formulas
• Propositional logic
• Simplest normal form

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(n3) of P(F) is much less than the complexity O(2n) of the true value table method and the complexity O(n5) of HAL based on the tactic scheme.

• 出版日期2008-9
• 单位华南理工大学