Cirquent calculus deepened

Abstract

Cirquent calculus is a new proof-theoretic and semantic framework, whose main distinguishing feature is being based on circuits, as opposed to the more traditional approaches that deal with tree-like objects such as formulas or sequents. Among its advantages are greater efficiency, flexibility and expressiveness. This paper presents a detailed elaboration of a deep-inference cirquent logic, which is naturally and inherently resource conscious. It shows that classical logic, both syntactically and semantically, is just a special, conservative fragment of this more general and, in a sense, more basic logic -- the logic of resources in the form of cirquent calculus. The reader will find various arguments in favor of switching to the new framework, such as arguments showing the insufficiency of the expressive power of linear logic or other formula-based approaches to developing resource logics, exponential improvements over the traditional approaches in both representational and proof complexities offered by cirquent calculus, and more. Among the main purposes of this paper is to provide an introductory-style starting point for what, as the author wishes to hope, might have a chance to become a new line of research in proof theory -- a proof theory based on circuits instead of formulas.

Significant improvements over the previous versions

References in corpus (3)

• Sequential operators in computability logic
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Computability Logic: a formal theory of interaction

Cited by in corpus (25)

• Sequential operators in computability logic
• On the Proof Complexity of Deep Inference
• A System of Interaction and Structure IV: The Exponentials and Decomposition
• Many concepts and two logics of algorithmic reduction
• The taming of recurrences in computability logic through cirquent calculus, Part I
• Toggling operators in computability logic
• From formulas to cirquents in computability logic
• Introduction to clarithmetic II
• In the beginning was game semantics
• Towards applied theories based on computability logic
• The parallel versus branching recurrences in computability logic
• A new face of the branching recurrence of computability logic
• On the system CL12 of computability logic
• A logical basis for constructive systems
• Introduction to clarithmetic I
• Separating the basic logics of the basic recurrences
• The Computational Complexity of Propositional Cirquent Calculus
• Elementary-base cirquent calculus I: Parallel and choice connectives
• Build your own clarithmetic I: Setup and completeness
• Ptarithmetic
• Soundness and completeness of the cirquent calculus system CL6 for computability logic
• The countable versus uncountable branching recurrences in computability logic
• A cirquent calculus system with clustering and ranking
• A propositional system induced by Japaridze's approach to IF logic
• Implementing program extraction from CL1-proofs