可计算性逻辑中CoL2系统的可判定性分析-论文.pdf

《可计算性逻辑中CoL2系统的可判定性分析-论文.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、第42卷第7期计算机科学Vo1．42No．72015年7月Coml~uterScienceJuly2015可计算性逻辑中CoL2系统的可判定性分析李兴香栾峻峰(山东大学计算机科学与技术学院济南250101)摘要可计算性(Computability)即算法有解性，是数学和计算机科学领域中重要的概念之一。可计算性逻辑(ComputabilityLogic，COL)是关于可计算性的形式理论，是一种交互的资源逻辑。其中，CoL2系统采用博弈的语义，是对经典命题逻辑的扩展，在经典命题逻辑的基础上添加了选择运算和一般原子，比经典命题逻辑更富有表达力，具有更广阔的应用前景，并且有较高的证明效率。分

2、析了COL2系统的可判定性，即通过提出一个算法来判断任意一个CoL2公式是否是可证明的，并且证明了该算法是多项式空间内运行的。关键词可计算性逻辑，COL2，交互计算，博弈语义中图法分类号TP301文献标识码ADOI10．i1896／j．issn．1002—137X2015．7．010ResearchonDecidabilityofCoL2inComputabilityLogicLIXing-xiangLUANJun-feng(DepartmentofComputerScienceandTechnology，ShandongUniversity，Jinan250101，China)Ab

3、stractComputabilityoralgorithmsolvablity，isoneoftheimportantconceptsinthefieldofmathematicsandcom-puterscience．Computahilitylogic(abbreviatedasCOL)isaformaltheoryofcomputabilityandaninteractiveresourcelogic．CoL2logicusesgamesemantics．CoL2isanextensionofclassicalpropositionallogic．WhatmakesCOL2m

4、oreex-pressivethanclassicalpropositionallogicisthepresenceofchoiceoperatorsandgeneralatom_CoL2hasahigherproofefficiency．Inthispaper，thedecidabilityofCOL2waspresented，inotherwords，bypresentinganalgorithmwhetheranyCoL2formulaisprovablecanbedetermined，andweprovedthatthealgorithmrunsinpolynomialspa

5、ce．KeywordsComputabilitylogic，CoL2，Interactivealgorithms，Gamesemantics经典逻辑是可计算性逻辑的一部分，这是因为经典逻辑1引言的谓词就是一类特殊的可计算问题——零交互的问题，而且可计算性(computability)即算法有解性，是数学和计算经典逻辑中的真(truth)的概念就相当于可计算问题中的可机科学领域中重要的概念之一。可计算性逻辑(Computabili—计算性的概念。因此可计算性逻辑是经典逻辑的扩展，而可tyLogic，CoL)是G．Japaridze在2003年提出的一种交互的计算性逻辑在应用理论方面更富

6、有表达力和建设性，并且有资源语义，是关于可计算性的形式理论[1]。较高的证明效率_l。CoL2在语义上采用“博弈”语义，是相较于经典逻辑“真文献[2，3，5，6]先后阐述了可计算性逻辑CoL的特殊部值”语义的一次质的改变。现实生活中的大多数计算问题是分COL1、CoL2、CoL3和CoL4，并且证明了它们的可靠性和用户与计算机之间复杂的多输入输出的交互过程，可计算问完备性，这为可计算性逻辑的应用提供了逻辑基础。本文在题的解决意味着计算机最终赢得了这个博弈，即输出了正确此基础上给出了CoL2系统的可判定性证明。的答案。因此，可将可计算问题等同于博弈问题删。可计2可计算性逻辑基础算性是可

7、计算问题的特性，问题的可计算性是指存在一台计算机赢得这个博弈。可计算问题也称为可计算任务，可以看本节简单介绍可计算性逻辑中的一些基本概念。作是两个角色(即计算机和外部环境)之间的博弈或对话。传可计算性逻辑中包含很多符号[7]，这里主要介绍以下符统的问题可以看作是一个简单博弈，这类博弈是由提出问题号：(1)个体常量符：a，b，C⋯；(2)个体变量符：z，Y，z⋯；(3)逻(输入input)和回答问题(输出output)组成的两步交互对话。辑常量符：T和上；(