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

论文摘要

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

论文目录

• 0 引言
• 1 Cm形式语言是递归可枚举的
• 2 单个公理模式所映射的公理集是递归可枚举集
• 3 Cm公理集是递归可枚举集
• 4 Cm的正向推理算法α
• 5 结论

文章来源

类型: 期刊论文

作者: 张伟

关键词: 系统,制约逻辑,可计算性,定理机器证明

来源: 辽宁大学学报(自然科学版) 2019年01期

年度: 2019

分类: 基础科学,哲学与人文科学,信息科技

专业: 数学,逻辑学,自动化技术

单位: 东北大学计算机科学与工程学院

基金: 辽宁省自然科学基金计划重点项目(20170540311),东北大学2017年本科教学质量工程项目(201755)

分类号: O141.1;TP18

DOI: 10.16197/j.cnki.lnunse.2019.01.005

页码: 31-37

总页数: 7

文件大小: 146K

下载量: 18