可计算性逻辑中若干Cirquent演算系统的研究

Computability logic (CoL), introduced recently, is a formal theory of computability. It has interactive game semantics, and is a logic of resources. Unlike the more traditional logics, it has greater expressiveness and higher efficiency, which makes it be potentially used in knowledgebase systems, systems for planning and action, verifying circuit equivalence etc. Cirquent calculus is the main method of CoL, and its main characteristics are allowing sharing subcomponents and deep inference, which is the reason that CoL has the above advantages. So in this work, we study on several cirquent calculus systems for CoL as follows: (1)to study different cirquent calculus systems corresponding to the different fragments of CoL; (2)to study the proof complexities of several cirquent calculus systems; (3)to give the definition of cirquent that has multiple roots and the corresponding inference system, so as to apply it in verifying circuit equivalence and optimizing circuits. In brief, this work is unique in topics and methods, and has important application values and prospects in computer science and digital design .

可计算性逻辑(CoL)是新近提出的关于可计算性的形式理论。它采取交互的博弈语义，同时也是一种资源逻辑。相比于传统逻辑，CoL具有表达能力强、证明效率高的优点，这使得它在知识库系统、人工智能行为规划、电路等价性验证等领域有着良好的应用前景和广阔的发展空间。Cirquent演算是CoL理论中的重要研究方法，其最大特点是允许分享子结构和采用深度推理，这是CoL理论具有上述优点的主要原因所在。因此，本项目拟对CoL中若干Cirquent演算系统进行研究，具体内容如下：(1)研究CoL不同逻辑部分相应的Cirquent演算系统；(2)研究若干Cirquent演算系统的证明复杂度问题；(3)给出多根Cirquent的定义及推理系统以应用于电路等价性验证和优化等问题中。本项目研究课题新颖、方法独特、内容详实，在计算机科学、电路设计等领域有着重要的理论指导意义和应用价值。

可计算性逻辑(CoL)是新近提出的关于可计算性的形式理论。它采取交互的博弈语义，同时也是一种资源逻辑。相比于传统逻辑，CoL具有表达能力强、证明效率高的优点，这使得它在知识库系统、人工智能行为规划、电路等价性验证等领域有着良好的应用前景和广阔的发展空间。Cirquent演算是CoL理论中的重要研究方法，其最大特点是允许分享子结构和采用深度推理，这是CoL理论具有上述优点的主要原因所在。本项目对CoL理论中的若干Cirquent演算系统进行了研究，具体内容如下：(1)研究带有Cluster的Cirquent演算系统；(2)研究同时带有Cluster和Rank的Cirquent演算系统；(3)研究带有复发算子的Cirquent演算系统的可判定性；(4)研究多根Cirquent演算系统在电路等价性验证与最优化问题中的应用。经过项目组成员的共同努力, 我们对上述研究内容取得的重要成果总结如下：(1)建立了带有∨-Cluster的Cirquent演算公理系统，使IF逻辑命题部分得到了真正意义上的公理化；(2)建立了带有∨-Cluster和2个Rank的Cirquent演算公理系统，解决了Extended IF逻辑命题水平的公理化问题；(3)建立了带有∧,∨-Cluster和任意有限个Rank的Cirquent演算公理系统，为Extended IF逻辑命题部分提供了一个保守扩张系统，它是我们前期提出的两个Cirquent演算系统的扩张，因此具有重要的理论和应用价值；(4)证明了带有复发算子的Cirquent演算系统CL15的可判定性。