可计算性逻辑中CoL2系统的可判定性分析
可计算性(computability),即算法有解性,是数学和计算机科学领域中重要的概念之一.可计算性逻辑(Computability Logic,CoL)是关于可计算性的形式理论,是一种交互的资源逻辑.其中,CoL2系统采用博弈的语义,是对经典命题逻辑的扩展,是在经典命题逻辑的基础上添加了选择运算和一般原子,比经典命题逻辑更富有表达力和更广阔的应用前景,并且有较高的证明效率.本文分析了CoL2系统的可判定性,即通过提出一个算法来判断任意一个CoL2公式是否是可证明的,并且证明了该算法是多项式空间内运行的.
计算机技术 CoL2系统 可计算性逻辑 交互计算 可判定性
李兴香 栾峻峰
山东大学计算机科学与技术学院 济南 250101
国内会议
济南
中文
1-6
2014-10-16（万方平台首次上网日期，不代表论文的发表时间）