命题逻辑定理证明的一个普遍能行算法

• 作者: 杨冠平
• 来源期刊: 信息工程大学学报
• 学科: 数学
• 关键词: 逻辑定理 机器证明 形式系统 推理规则 等值置换
• 年，卷（期）: 2003,（4）
• 页码范围: 29-32
• 页数: 4页
• 分类号: O141
• 字数: 4100字
• 语种: 中文
• DOI: 10.3969/j.issn.1671-0673.2003.04.008

摘要

本文以等值置换为推理规则,以交换律、结合律、分配律、吸真律和排中律为公理建立一命题逻辑形式系统.在此基础上给出一机器能行算法,把排中律等值置换成任一重言式,证明任一命题逻辑内定理.也引申出命题逻辑定理证明的一个可信性问题.