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

A Mechanical Theorem Proving System for C_m Propositional Calculus

作　　者：张伟 ZHANG Wei(College of Computer Sci.and Eng. ,Northeastern University,Shenyang 110819,China)

机构地区：[1]东北大学计算机科学与工程学院,辽宁沈阳110169

出　　处：《辽宁大学学报（自然科学版）》2019年第1期31-37,共7页Journal of Liaoning University：Natural Sciences Edition

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

摘　　要：C_m系统是制约逻辑的命题演算系统,但是其推导定理的过程可否由图灵(计算机)算法完成尚未得到明确的结论.研究证明了C_m的公式集是递归可枚举集,并且给出了一个递归枚举算法,该算法能够对任一给定的实际可证的C_m式在有限的步骤内判定它属于C_m可证公式集.并给出了C_m命题演算系统的一个定理机器证明系统.因此证明了C_m系统至少是半可判定的.The Cm system is a propositional calculus system for Entailment logic,but the (Turing) computability of its theorem derivation has not been proved yet.In this paper,it is proved that the formula set of Cm is recursively enumerable (r.e.),and an enumeration algorithm is presented,which can be used to determine that,for any given actual provable Cm formula u , u is a valid formula in finite number of steps.This paper presents a mechanical theorem proving system for the C m propositional calculus.Therefore,it is proved that the Cm system is at least semi-decidable.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]