论文部分内容阅读
消解算法对命题逻辑定理自动证明是普遍能行的,但现行消解证明只能归属于反证法.本文提出直证式消解原理,从析取范式能否消解出最简恒真式来判定和证明定理.其消解规则是原消解规则的对偶定理,消解过程中每步得式也都是原消解过程相应得式的否定式.只须赋予新的逻辑涵义,消解的集合表达形式仍可使用.直证式消解算法也具有可靠性、完全性、能行性,然而剔除了反证步骤,更简明直接.