可计算性逻辑中CoL2系统的可判定性分析

摘要：

可计算性(Computability)即算法有解性,是数学和计算机科学领域中重要的概念之一.可计算性逻辑(Computability Logic,CoL)是关于可计算性的形式理论,是一种交互的资源逻辑.其中,CoL2系统采用博弈的语义,是对经典命题逻辑的扩展,在经典命题逻辑的基础上添加了选择运算和一般原子,比经典命题逻辑更富有表达力,具有更广阔的应用前景,并且有较高的证明效率.分析了CoL2系统的可判定性,即通过提出一个算法来判断任意一个CoL2公式是否是可证明的,并且证明了该算法是多项式空间内运行的.

关键词：可计算性逻辑、CoL2、交互计算、博弈语义

所属期刊栏目：42

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金项目61202014

在线出版日期：2016-05-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：44-47