论文摘要
C_m系统是制约逻辑的命题演算系统,但是其推导定理的过程可否由图灵(计算机)算法完成尚未得到明确的结论.研究证明了C_m的公式集是递归可枚举集,并且给出了一个递归枚举算法,该算法能够对任一给定的实际可证的C_m式在有限的步骤内判定它属于C_m可证公式集.并给出了C_m命题演算系统的一个定理机器证明系统.因此证明了C_m系统至少是半可判定的.
论文目录
文章来源
类型: 期刊论文
作者: 张伟
关键词: 系统,制约逻辑,可计算性,定理机器证明
来源: 辽宁大学学报(自然科学版) 2019年01期
年度: 2019
分类: 基础科学,哲学与人文科学,信息科技
专业: 数学,逻辑学,自动化技术
单位: 东北大学计算机科学与工程学院
基金: 辽宁省自然科学基金计划重点项目(20170540311),东北大学2017年本科教学质量工程项目(201755)
分类号: O141.1;TP18
DOI: 10.16197/j.cnki.lnunse.2019.01.005
页码: 31-37
总页数: 7
文件大小: 146K
下载量: 18
相关论文文献
- [1].几何定理机器证明三十年[J]. 系统科学与数学 2009(09)
- [2].几何定理机器证明的并行前向推理[J]. 华南理工大学学报(自然科学版) 2008(04)
- [3].科技创新正在更新教学[J]. 科技导报 2020(10)
- [4].天堑变通途——《初等几何研究(第2版)》代序[J]. 高等数学研究 2015(05)
- [5].HORN集上基于广义归结方法的定理机器证明[J]. 湘潭师范学院学报(自然科学版) 2009(01)
- [6].《中国学术期刊文摘》综述文摘选登[J]. 科技导报 2010(10)
- [7].本体推理在几何定理机器证明中的应用[J]. 计算机技术 与发展 2013(09)
- [8].例证法思想在高等职业院校高数教学中的应用研究[J]. 和田师范专科学校学报 2008(04)
- [9].SGARP中符号计算模块的实现及其应用[J]. 计算机研究与发展 2014(06)
- [10].改进的几何定理机器证明的概率性算法[J]. 计算机应用 2014(07)
- [11].论文外流探因[J]. 黑龙江科学 2013(08)
- [12].基于拼凑替换的定理机器证明的研究与实现[J]. 计算机技术与发展 2012(06)
- [13].一种新的基于扩展规则的定理证明算法[J]. 计算机研究与发展 2009(01)
- [14].通化师范学院学人——李武明教授[J]. 通化师范学院学报 2011(08)
- [15].基于IMOM和IBOHM启发式策略的扩展规则算法[J]. 软件学报 2009(06)
- [16].信念修正开放过程模式可判定公式表达能力[J]. 吉林大学学报(工学版) 2016(06)