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

摘要：

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

关键词：命题逻辑、公式判定、演绎判定、自动定理证明

所属期刊栏目：36

分类号：TP301.2(计算技术、计算机技术)

在线出版日期：2008-12-09（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：71-76