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