This paper is a brief presentation of cirquent calculus, a novel proof system for resource-conscious logics. As such, it is a refinement of sequent calculus with mechanisms that allow to explicitly account for the possibility of sharing of subexpressions/subresources between different expressions/resources. This is achieved by dealing with circuit-style constructs, termed cirquents, instead of formulas, sequents or other tree-like structures. The approach exhibits greater expressiveness, flexibility and efficiency compared to the more traditional proof-theoretic approaches. The need for substantially new deductive tools that could overcome the limitations of sequent calculus while dealing with resource logics surfaced with the birth of computability logic, a game-semantically conceived logic of computational resources and tasks, acting as a formal theory of computability in the same sense as classical logic is a formal theory of truth.Cirquent calculus offers elegant axiomatizations for certain basic fragments of computability logic that have been shown to be inherently unaxiomatizable in sequent calculus or other traditional systems. The paper provides an iformal account on the main characteristic features of cirquent calculus, motivations for it, semantics, advantages over sequent calculus, as well as how cirquent calculus relates to classical and linear logics. Out of several existing cirquent calculus systems, only the simplest and most basic one, CL5, is presented in full detail.
Copyright (c) 2022 Giorgi Japaridze
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
Blass, A. "A game semantics for linear logic", Annals of Pure and Applied Logic, 1992, Vol. 56, pp. 183-220.
Das, A., Strassburger, L. "On linear rewriting systems for Boolean logic and some applications to proof theory", Logical Methods in Computer Science, 2016, Vol. 12, pp. 1-27.
Japaridze, G. "Introduction to computability logic", Annals of Pure and Applied Logic, 2003, Vol. 123, pp. 1-99.
Japaridze, G. "Introduction to cirquent calculus and abstract resource semantics", Journal of Logic and Computation, 2006, Vol. 16, pp. 489-532.
Japaridze, G. "Cirquent calculus deepened", Journal of Logic and Computation, 2008, Vol. 18, pp. 983-1028. Japaridze, G. "From formulas to cirquents in computability logic", Logical Methods is Computer Science, 2011, Vol. 7, Issue 2 , Paper 1, pp. 1-55.
Japaridze, G. ``The taming of recurrences in computability logic through cirquent calculus, Part I", Archive for Mathematical Logic, 2013, Vol. 52, pp. 173-212.
Japaridze, G. ``The taming of recurrences in computability logic through cirquent calculus, Part II", Archive for Mathematical Logic, 2013, Vol. 52, pp. 213-259.
Japaridze, G. ``Elementary-base cirquent calculus I: Parallel and choice connectives",
Journal of Applied Logics - IfCoLoG Journal of Logics and their Applications, 2018, Vol. 5, no.1, pp. 367-388.
Japaridze, G. ``Elementary-base cirquent calculus II: Choice quantifiers", Logic Journal of the IGPL, 2020, jzaa022, https://doi.org/10.1093/jigpal/jzaa022 .
Japaridze, G. ``Fundamentals of computability logic 2020", IfCoLog Jpurnal of Logics and their Applications, 2020, Vol. 7, pp. 1177-1198.
Xu, W., Liu, S. ``Soundness and completeness of the cirquent calculus system CL6 for computability logic", Logic Journal of the IGPL, 2012, Vol. 20, pp. 317-330.
Xu, W. ``A propositional system induced by Japaridze's approach to IF logic", Logic Journal of the IGPL, 2014, Vol. 22, pp. 982-991.
Xu, W. ``A cirquent calculus system with clustering and ranking", Journal of Applied Logic, 2016, Vol. 16, pp. 37-49.