Journal of South China University of Technology (Natural Science Edition) ›› 2008, Vol. 36 ›› Issue (9): 71-76.

• Computer Science & Technology • Previous Articles     Next Articles

A Deduction-Based Decision Method of Propositional Formulas

Qi De-yu  Li Xiao-xin   

  1. School of Computer Science and Engineering, South China University of Technology, Guangzhou 510640, Guangdong, China
  • Received:2007-10-08 Revised:2008-04-24 Online:2008-09-25 Published:2008-09-25
  • Contact: 齐德昱（1959-），男，教授，博士生导师，主要从事网格计算、计算机系统结构、大型软件开发方法等研究． E-mail:qideyu@scut．edu．cn
  • About author:齐德昱（1959-），男，教授，博士生导师，主要从事网格计算、计算机系统结构、大型软件开发方法等研究．

PDF

818

Abstract:

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 complexityO （ 2n ） of the true value table method and the complexity O（ n5 ） of HAL based on the tactic scheme.

Key words: propositional logic, formula decision, deduction-based decision, automatic theorem proving