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

华南理工大学学报（自然科学版） ›› 2008, Vol. 36 ›› Issue (9): 71-76.

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

齐德昱李小薪

华南理工大学计算机科学与工程学院, 广东广州 510640

收稿日期:2007-10-08 修回日期:2008-04-24 出版日期:2008-09-25 发布日期:2008-09-25
通信作者: 齐德昱（1959-），男，教授，博士生导师，主要从事网格计算、计算机系统结构、大型软件开发方法等研究． E-mail:qideyu@scut．edu．cn
作者简介:齐德昱（1959-），男，教授，博士生导师，主要从事网格计算、计算机系统结构、大型软件开发方法等研究．

A Deduction-Based Decision Method of Propositional Formulas

Qi De-yu Li Xiao-xin

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-），男，教授，博士生导师，主要从事网格计算、计算机系统结构、大型软件开发方法等研究．

摘要/Abstract

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

关键词: 命题逻辑, 公式判定, 演绎判定, 自动定理证明

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（ n³） of P（F） is much less than the complexityO （ 2ⁿ ） of the true value table method and the complexity O（ n⁵ ） of HAL based on the tactic scheme.

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

齐德昱李小薪. 命题公式的一种演绎判定方法[J]. 华南理工大学学报（自然科学版）, 2008, 36(9): 71-76.

Qi De-yu Li Xiao-xin. A Deduction-Based Decision Method of Propositional Formulas[J]. Journal of South China University of Technology (Natural Science Edition), 2008, 36(9): 71-76.