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

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