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

命题公式的判定是人工智能领域中的一个核心问题。目前命题公式的判定方法大都是基于语义的，不能给出演绎过程，而这种演绎过程是许多推理性应用的重要依据，本文针对命题演算系统L，给出了一种可同时给出演绎过程的判定方法——演绎判定方法。首先提出了消解复杂性的两种范式：最简范式和文字范式，在此基础上给出了L的可判性定理的演绎证明及命题公式的演绎判定算法P(F)，并基于ML语言设计了基于P(F)的演绎判定机DMBD。

A Decision Method Based on Deduction for Propositional Formulas

Propositional formulas decision is one of core issues in artificial intelligence field. However, most of present decision methods are based on semantics and cannot give deduction procedure which is an important reference in many reasoning application. Based on formal system L of proposition calculus, a decision method based on deduction for propositional formulas, which can give the deduction procedure, is given in this paper. Two normal forms, best-simple normal form and literal normal form, are presented at first in order to eliminate the complexity of formulas decision. Based on the two normal forms, a deduction proof of decidability theorem in L and a decision algorithm P(F) based on deduction for proportional formulas are given and a decision machine found on P(F), DMBD, is also designed.