Cirquent calculus is a

proof calculus In mathematical logic, a proof calculus or a proof system is built to prove statements. Overview A proof system includes the components: * Language: The set ''L'' of formulas admitted by the system, for example, propositional logic or first-order ...

that manipulates graph-style constructs termed ''cirquents'', as opposed to the traditional tree-style objects such as

formula In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwee ...

s or

sequent In mathematical logic, a sequent is a very general kind of conditional assertion. : A_1,\,\dots,A_m \,\vdash\, B_1,\,\dots,B_n. A sequent may have any number ''m'' of condition formulas ''Ai'' (called " antecedents") and any number ''n'' of asse ...

s. Cirquents come in a variety of forms, but they all share one main characteristic feature, making them different from the more traditional objects of syntactic manipulation. This feature is the ability to explicitly account for possible sharing of subcomponents between different components. For instance, it is possible to write an expression where two subexpressions ''F'' and ''E'', while neither one is a subexpression of the other, still have a common occurrence of a subexpression ''G'' (as opposed to having two different occurrences of ''G'', one in ''F'' and one in ''E'').

Overview

The approach was introduced by G. Japaridze in as an alternative proof theory capable of "taming" various nontrivial fragments of his

computability logic Computability logic (CoL) is a research program and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic which is a formal theory of truth. It was introduced and so named by G ...

, which had otherwise resisted all axiomatization attempts within the traditional proof-theoretic frameworks. The origin of the term “cirquent” is CIRcuit+seQUENT, as the simplest form of cirquents, while resembling circuits rather than formulas, can be thought of as collections of one-sided

s (for instance, sequents of a given level of a Gentzen-style proof tree) where some sequents may have shared elements. Cirquent_for_the_

The basic version of cirquent calculus in was accompanied with an "''abstract resource semantics''" and the claim that the latter was an adequate formalization of the resource philosophy traditionally associated with

linear logic Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter. Although the logic has also be ...

. Based on that claim and the fact that the semantics induced a logic properly stronger than (affine) linear logic, Japaridze argued that linear logic was incomplete as a logic of resources. Furthermore, he argued that not only the deductive power but also the expressive power of linear logic was weak, for it, unlike cirquent calculus, failed to capture the ubiquitous phenomenon of resource sharing. Linear_logic_vs_classical_logic

The resource philosophy of cirquent calculus sees the approaches of

and

classical logic Classical logic (or standard logic or Frege-Russell logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy. Characteristics Each logical system in this class ...

as two extremes: the former does not allow any sharing at all, while in the latter “everything is shared that can be shared”. Unlike cirquent calculus, neither approach thus permits mixed cases where some identical subformulas are shared and some not. Among the later-found applications of cirquent calculus was the use of it to define a semantics for purely propositional

independence-friendly logic Independence-friendly logic (IF logic; proposed by Jaakko Hintikka and in 1989) is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form (\exists v/V) and (\forall v/V), where V is a finite set of variables. ...

. The corresponding logic was axiomatized by W. Xu. Syntactically, cirquent calculi are

deep inference Deep inference names a general idea in structural proof theory that breaks with the classical sequent calculus by generalising the notion of structure to permit inference to occur in contexts of high structural complexity. The term ''deep inferen ...

systems with the unique feature of subformula-sharing. This feature has been shown to provide speedup for certain proofs. For instance, polynomial size

analytic proof In mathematics, an analytic proof is a proof of a theorem in analysis that only makes use of methods from analysis, and which does not predominantly make use of algebraic or geometrical methods. The term was first used by Bernard Bolzano, who first ...

s for the propositional pigeonhole have been constructed. Only quasipolynomial analytic proofs have been found for this principle in other deep inference systems. In resolution or analytic Gentzen-style systems, the

pigeonhole principle In mathematics, the pigeonhole principle states that if items are put into containers, with , then at least one container must contain more than one item. For example, if one has three gloves (and none is ambidextrous/reversible), then there mu ...

is known to have only exponential size proofs.A. Haken, �
The intractability of resolution
��. Theoretical Computer Science 39 (1985), pp. 297–308.

References

Literature

*M.Bauer, �
The computational complexity of propositional cirquent calculus
��. Logical Methods in Computer Science 11 (2015), Issue 1, Paper 12, pp. 1–16. *G.Japaridze, �
Introduction to cirquent calculus and abstract resource semantics
��. Journal of Logic and Computation 16 (2006), pp. 489–532. *G.Japaridze, �
Cirquent calculus deepened
” Journal of Logic and Computation 18 (2008), pp. 983–1028. * G.Japaridze, �
From formulas to cirquents in computability logic
��. Logical Methods in Computer Science 7 (2011), Issue 2, Paper 1, pp. 1–55. *G.Japaridze, �
The taming of recurrences in computability logic through cirquent calculus, Part I
��.Archive for Mathematical Logic 52 (2013), pages 173–212. * G.Japaridze
“The taming of recurrences in computability logic through cirquent calculus, Part II
�� Archive for Mathematical Logic 52 (2013), pages 213–259. *I. Mezhirov and N. Vereshchagin,
On abstract resource semantics and computability logic
'. Journal of Computer and System Sciences 76 (2010), pp. 356–372. *W.Xu and S.Liu, �
Soundness and completeness of the cirquent calculus system CL6 for computability logic
��. Logic Journal of the IGPL 20 (2012), pp. 317–330. *W.Xu and S.Liu, �
Cirquent calculus system CL8S versus calculus of structures system SKSg for propositional logic
��. In: Quantitative Logic and Soft Computing. Guojun Wang, Bin Zhao and Yongming Li, eds. Singapore, World Scientific, 2012, pp. 144–149. *W.Xu, �
A propositional system induced by Japaridze's approach to IF logic
��. Logic Journal of the IGPL 22 (2014), pages 982–991. *W. Xu,
A cirquent calculus system with clustering and ranking
'. Journal of Applied Logic 16 (2016), pp. 37–49.

External links

* Logical calculi Proof theory Logical expressions Non-classical logic {{logic-stub