可计算性(computability),即算法有解性,是数学和计算机科学领域中最重要的概念之一。可计算性逻辑(Computability Logic,简写为CoL)是研究可计算性的形式理论,它将问题看作是计算机(或者以计算机为表现形式的人)与外部环境之间的博弈,问题的可计算性是指存在一台计算机能赢得这个博弈。传统逻辑主要回答什么是永真的、有效的,而可计算性逻辑试图系统的回答什么是可计算的及应如何计算。CoL中的公式代表交互计算问题,逻辑运算代表在可计算问题上的交互操作,一个公式是有效的是指存在解决相应问题的方法(或者等价的,存在赢得博弈的策略)。本文首先介绍了可计算性逻辑的博弈语义及其形式化的定义,给出了CoL中的(?)、(?)、(?)、(?)、(?)和→等逻辑运算表达的意义及其形式化定义。博弈分为静态博弈和动态博弈,静态博弈是与博弈双方反应速度无关的博弈,其最终结果只取决于博弈的策略。CoL所研究的博弈问题都是静态博弈。HPM (hard-play machine)是交互计算机模型的最基本模型,它是在一种图灵机模型基础上修改得到的计算机模型。另一种计算模型是EPM (easy-play machine),它与HPM在设计上唯一的区别在于只有当计算机明确的允许环境行动时环境才可以做一个行动。对于静态博弈问题来说,这两种模型是等价的。在实际解决问题的过程中,我们更倾向于采用EPM模型。CL2逻辑采用博弈的语义,是对经典命题逻辑的保守扩展,比经典命题逻辑更富有表达力和更广阔的应用前景,并且有较高的证明效率。与经典命题逻辑相比,CL2逻辑包含两类原子：简单原子和一般原子。简单原子代表简单计算问题,它与经典命题逻辑中的谓词相对应；一般原子代表一般的交互计算问题,在意义上有别于谓词。经典逻辑的真的概念就相当于CL2中的可计算性的概念。CL2逻辑系统已经被证明了是完备的、可靠的逻辑系统。本文的创新点在于：(1).分析CL2系统的可判定性。提出判断CL2公式可证明性的算法,并且证明该算法是多项式空间内运行的。(2).分析CL2系统的空间复杂性。通过将PSPACE完全问题——量词化布尔公式(Truth of Quantified Boolean Formula,简写为TQBF)问题归约到CL2公式的可证明性问题,我们证明了CL2系统是PSPACE完全的。这样结果表明了CL2公式的可证明性问题是比NP-hard更难的一类问题。