可计算性逻辑是新近提出的关于可计算性的形式理论.它采取交互的博弈语义,是一种资源逻辑.经典逻辑、直觉逻辑和线性逻辑(在广义上)只是可计算性逻辑的三个特殊部分.相比于传统逻辑,可计算性逻辑具有更强的表达能力和更高的证明效率,这使得它有望在知识库系统、人工智能行为规划系统、电路等价性验证等领域得到广泛的应用.本文主要利用可计算性逻辑的Cirquent演算方法,对其若干形式系统及算子进行了研究,主要工作和创新概括如下：●证明了Cirquent演算系统CL6关于可计算性逻辑语义的可靠性与完备性.首先给出与证明相关的所有语法定义；然后利用形式系统CL2关于可计算性逻辑语义的可靠完备性,间接地从语法角度证明了系统CL6的可靠完备性,从而得到既是经典命题逻辑又是Cirquent演算系统CL5的扩张.●揭示了平行复发算子与不可数分支复发算子的关系.首先给出关于平行复发算子的Cirquent演算系统；其次定义关于平行复发算子的Cirquent的语义;然后在此定义基础上证明关于平行复发算子的Cirquent演算系统的可靠性,得到由不可数分支复发算子诱导的逻辑是由平行复发算子诱导的逻辑的真子集；最后,在不可数分支复发逻辑蕴含平行复发但反之不成立的意义下,得到平行复发算子严格地弱于不可数分支复发算子,至此彻底搞清了这两个算子自提出以来模糊不清的关系.●揭示了可数分支复发算子与不可数分支复发算子的关系.首先给出可数分支复发算子新的简化定义,证明该定义与旧定义的逻辑等价性；然后定义关于可数分支复发算子的Cirquent的语义,并在此基础上证明关于可数分支复发算子的Cirquent演算系统的可靠性,得到由不可数分支复发算子诱导的逻辑是由可数分支复发算子诱导的逻辑的真子集;最后得到可数分支复发算子严格地弱于不可数分支复发算子.同样,这使得可数与不可数分支复发算子的关系彻底明了化.●基于可计算性逻辑Cirquent演算方法的优越性,为命题逻辑公式提出一种压缩表达方式,并证明基于该表达的命题逻辑系统比传统相继式演算系统Gentzen{cut}的证明效率有指数级的提高,从而为经典命题逻辑提供了一个可靠完备的但证明效率较高的形式系统.其次,研究Cirquent演算系统CL8S的性质,证明其中的演绎定理成立,并对比CL8S与结构演算系统SKSg的证明复杂度,得到CL8S限制在命题逻辑水平p-仿真SKSg.·基于可计算性逻辑博弈语义的优越性,分析了可计算性逻辑有望取代经典逻辑作为知识库系统逻辑基础的优越性与可行性,并以可计算性逻辑的完备子集CL4为基础进行知识表示和推理,设计出正反结合的推理机,通过实例显示出能够表达更细致知识、便于人机交互等优点.