Cm命题演算的定理机器证明系统

• 作者: 张伟
• 来源期刊: 辽宁大学学报（自然科学版）
• 学科: 工学
• 关键词: Cm系统 制约逻辑 可计算性 定理机器证明
• 年，卷（期）: 2019,（1）
• 所属期刊栏目: 信息科学与技术
• 页码范围: 31-37
• 页数: 7页
• 分类号: TP311
• 字数: 4166字
• 语种: 中文

摘要

Cm系统是制约逻辑的命题演算系统,但是其推导定理的过程可否由图灵(计算机)算法完成尚未得到明确的结论.研究证明了Cm 的公式集是递归可枚举集,并且给出了一个递归枚举算法,该算法能够对任一给定的实际可证的Cm 式在有限的步骤内判定它属于Cm 可证公式集.并给出了Cm 命题演算系统的一个定理机器证明系统.因此证明了Cm 系统至少是半可判定的.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张伟	东北大学计算机科学与工程学院	93	442	12.0	16.0