可计算性逻辑(Computability Logic)简称CoL,是由Japaridze首先提出的,它将经典逻辑中的真值理论发展成为可计算性的正式理论,是对经典逻辑的发展。在CoL中,我们将可计算性的问题看成是由机器和环境两种角色参加的博弈,问题的可计算性表示存在一个交互图灵机总能在表示这个问题的博弈中取胜；逻辑运算符代表可计算性问题上的运算；逻辑公式的永真性表示是永远可计算的问题。在对博弈和博弈运算的研究中,博弈运算的静态属性是可计算性逻辑中最基础也是非常重要的内容。在CoL中,我们更多关注的是参加博弈的角色在博弈进行过程中会做出什么动作,采取什么策略实现在博弈中取胜,而不关注他们的博弈速度,这就是静态博弈的含义。我们称一个博弈A是静态的,当且仅.当对于博弈的角色(机器或者环境)(?),博弈过程中产生的行程△和r,△是Γ的(?)-延迟,如果Γ是A中的一个使得(?)取胜的行程,那么△也是一个使得(?)取胜行程。因为在CoL中我们研究的博弈都是静态博弈,所以,每一个CoL中的运算都需要具有静态属性。CoL是经典逻辑的扩展,其运算符的语义在CoL中与经典逻辑的语义是一致的。目前,随着CoL的发展,研究者们已经提出了很多新的运算符,其中分支切换(补)复用运算((?)和(?))是目前最难也是最复杂的一种运算。Japaridze已经给出了关于该运算的定义描述,但是没有给出其静态属性证明。这个问题也成为了CoL中的open问题之一。所以,本文主要研究了以下三个问题：切换分支复用运算的静态属性证明、新的切换分支复用运算的静态属性证明、新旧版本的切换分支复用运算的等价性证明。本文给出了正式的分支切换(补)复用运算的定义,在该定义中,我们采用静态博弈的(Lr, Wn)偶对完成了该运算的定义；并且在定义的基础上给出了该运算的静态性证明。证明过程中,我们首先给出了已知结点、外层已知结点的定义。根据证明的需要,我们使用了CoL中的行程延迟的概念。行程延迟是指在整个博弈过程中,参加博弈的机器或者环境会由于各种原因而导致在某个行程中出现一些运算步的延迟。本文给出了一个引理证明,证明了对于一个已知的静态博弈A,如果在(?)A的某一个行程△中由机器或者环境做出了一个非法的步,而且△是r的一个延迟,那么r也是(?)A一个非法步。在(?)和(?)的静态属性证明中,我们使用该引理的结论,简化了△和r在出现非法步时的分析,从而完成了分支切换复用运算的静态属性证明。由于(?)和(?)运算定义的复杂性,使得基于(?)和(?)的推导演绎系统以及应用系统的研究非常迟缓,这也影响了整个CoL研究的进程。所以,我们需要改进传统的(?)和(?)定义,试图寻找更简单的定义。本文提出了一个新的简单的(?)和(?)定义,为了区分之前的传统定义,我们称传统的定义为紧凑版,新的定义称为宽松版。采用(?)T,(?)T分别表示(?)和(?)的紧凑版,使用(?)L,(?)L分别表示(?)和(?)的宽松版。宽松版的分支切换复用运算定义采用位串表示方法,改变了紧凑版定义中对结点的依赖。本文根据定义也完成了宽松版的静态属性证明。在证明中,我们发现使用宽松版定义的分支切换复用运算需要考虑的情况明显减少,利于后续基于该运算的研究。本文介绍了两个版本的分支切换复用运算,为了在后续的基于分支切换复用运算推演系统和应用研究中使用宽松版的分支切换复用运算,我们需要给出两种版本运算的等价性证明。论文中,我们设计了两个交互算法证明了两种版本运算的等价性。由于CoL是基于博弈的交互计算,所以,我们使用了基于交互计算的图灵机模型-易交互计算模型(Easy-Play Machine)。通过该交互计算模型,我们给出了在CoL中可计算性问题求解步骤、行程和步的产生过程。运算等价性证明的第一个算法是指存在一个EPM ε1在博弈(?)TA→(?)LA即(?)T(?)A∨(?)LA中取胜。我们根据博弈设计了一个取胜策略,使得ε1存在并且能够取胜。第二个算法中,我们设计了一个EPMε2,使得它能在博弈(?)L(?)A∨(?)TA中取胜。我们也设计了一个取胜策略,证明这样的ε2存在。本文的主要研究工作和创新点：一、正式的分支切换复用运算的定义和静态属性证明1.我们给出了基于(Lr,Wn)偶对表示形式的分支切换(补)复用运算的定义。该定义主要是基于树形结构的思想,重点针对分支切换复用运算的分支运算和切换运算进行描述。所以,我们将分支运算中已知结点的概念进行了重新的定义,细化给出了外层已知结点的定义。定义了完成分支运算的结点只能是外层已知结点；完成切换运算的可以是任何已知结点。本文在行程延迟概念的基础上,给出了静态属性证明。借助于引理的结果,我们只需要分析两个具有延迟关系的行程。即一个静态博弈A,如果一个行程Γ是(?)A中的一个(?)取胜行程,那么其(?)-延迟行程△也是(?)A中的(?)取胜行程。从而证明了(?)是静态的。二、新的分支切换复用运算的定义和静态属性证明2.我们根据传统的分支切换(补)复用运算定义,采用基于位串的表示方法,给出了一个新的简单版本定义。该定义打破了已知结点的考虑和限制,定义中直接不需要考虑分支运算,简化了整个运算。完成运算定义之后,我们同样给出了新的分支切换复用运算的静态属性证明。在整个证明过程中,我们发现需要考虑和处理的情况明显减少,利于基于分支切换复用运算的一些演绎系统和应用系统的提出。三、两种版本运算等价性证明3.博弈的交互计算特点需要提出新的交互计算模型的概念,根据应用场合不同,论文介绍了难交互计算模型和易交互计算模型,通过这两种计算模型,我们可以理解博弈的进行过程、步和行程的产生过程。在论文中,我们选用对于机器来说更简单的易交互计算模型。事实上,两种计算模型在计算能力上是等价的。4.运算的等价性证明,是指在CoL中设计基于易交互计算模型的算法,使得机器在博弈运算中取胜。论文中设计了两个算法。在第一个算法中,我们证明存在一个EPMε1在博弈(?)T(?)A∨(?)LA中取胜。第二个算法,我们证明了存在一个EPMε2,使得ε2在博弈(?)L(?)A∨(?)TA中存在取胜策略。从而实现了运算的等价性证明。本文的进一步工作主要包括以下几个方面：1.我们计划设计基于宽松版分支切换(补)复用运算的推理系统。包括给出推理系统的推导原则、新的系统的可靠性和完整性证明。我们计划参考Japaridze提出的CL1-CL15的相关证明方法,设计新的CLx推理系统。2.实现基于分支切换(补)复用运算的应用系统。设计与实现CoL的应用系统,实现真正的人机交互运算。为CoL走向具体应用来设计平台和界面。我们已经设计和实现完成了CL1的交互计算应用,这可以为我们的研究提供基础。3.发现不同的计算机应用领域。CoL可以应用在交互计算、网络协议、知识库系统和基于资源的规划系统中。我们需要在这些领域中发现基于分支切换(补)复用运算的实际应用。