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

摘要：

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

关键词：Cm系统、制约逻辑、可计算性、定理机器证明

所属期刊栏目：46

分类号：TP311(计算技术、计算机技术)

资助基金：辽宁省自然科学基金计划重点项目20170540311;东北大学2017年本科教学质量工程项目201755

在线出版日期：2019-07-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：31-37