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

• 作者: 杨冠平
• 来源期刊: 信息工程大学学报
• 学科: 数学
• 关键词: 逻辑定理 自动证明 直证式 消解原理 能行算法
• 年，卷（期）: 2004,（4）
• 所属期刊栏目: 数学、信息安全
• 页码范围: 32-34
• 页数: 3页
• 分类号: O141
• 字数: 3211字
• 语种: 中文
• DOI: 10.3969/j.issn.1671-0673.2004.04.010

摘要

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