|
|||||
|
|
| Cm命题演算的定理机器证明系统 | |
| 作者姓名： | 张伟 |
| 作者单位： | 东北大学 计算机科学与工程学院,辽宁 沈阳,110169 |
| 基金项目： | 辽宁省自然科学基金;本科教学质量工程项目 |
| 摘 要： | C_m系统是制约逻辑的命题演算系统,但是其推导定理的过程可否由图灵(计算机)算法完成尚未得到明确的结论.研究证明了C_m的公式集是递归可枚举集,并且给出了一个递归枚举算法,该算法能够对任一给定的实际可证的C_m式在有限的步骤内判定它属于C_m可证公式集.并给出了C_m命题演算系统的一个定理机器证明系统.因此证明了C_m系统至少是半可判定的. |
| 关 键 词： | Cm系统 制约逻辑 可计算性 定理机器证明 |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |