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

项目名称： 可计算性逻辑中若干Cirquent演算系统的研究

项目编号： No.61303030

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 许文艳

作者单位： 西安电子科技大学

项目金额： 23万元

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

中文关键词： 可计算性逻辑；博弈语义；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 .

英文关键词： Computability Logic；Game Semantics；Cirquent Calculus；Resource Logic；Deep Inference