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