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

作者：齐德昱; 李小薪

来源：华南理工大学学报(自然科学版), 2008, (09): 71-76.

• 命题逻辑
• 公式判定
• 演绎判定
• 自动定理证明 propositional logic
• formula decision
• deduction-based decision
• automatic theorem proving

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

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