命题逻辑定理自动证明的直证式消解原理

Principle of Direct-Proof Resolution for Automatic Propositional Logic Theorems Proving

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

The method of resolution is universally effective to prove inner theorems of propositional logic automatically,but current one is a refutation procedure.In this paper,a principle of direct-proof resolution is presented,by which the theorems are decided and proved just on the basis of educing a simplest tautology from their disjunctive normal forms.Its resolution rule is duality theorem of old one.Each formula in new resolution processes is the negation formula of that in old resolution.The set form of resolution can still be used,as new logic meaning explains it properly.The algorithm of direct-proof resolution remains soundness,completeness and effectiveness.And abandoning the apagogic steps,it is more simple and direct.