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: * Formal language: The set ''L'' of formulas admitted by the system, for example, propositional logic or fir ...

that manipulates

graph Graph may refer to: Mathematics *Graph (discrete mathematics), a structure made of vertices and edges **Graph theory, the study of such graphs and their properties *Graph (topology), a topological space resembling a graph in the sense of discret ...

-style constructs termed ''cirquents'', as opposed to the traditional

tree In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, e.g., including only woody plants with secondary growth, only ...

-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 betwe ...

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 ass ...

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. JaparidzeG.Japaridze, �
Introduction to cirquent calculus and abstract resource semantics
��.

Journal of Logic and Computation A journal, from the Old French ''journal'' (meaning "daily"), may refer to: *Bullet journal, a method of personal organization *Diary, a record of personal secretive thoughts and as open book to personal therapy or used to feel connected to onesel ...

16 (2006), pp. 489–532. 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 ...

, 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. The basic version of cirquent calculus 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 French logician 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 ...

. 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 c ...

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 or The Deep may refer to: Places United States * Deep Creek (Appomattox River tributary), Virginia * Deep Creek (Great Salt Lake), Idaho and Utah * Deep Creek (Mahantango Creek tributary), Pennsylvania * Deep Creek (Mojave River tributary ...

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

polynomial In mathematics, a polynomial is a Expression (mathematics), mathematical expression consisting of indeterminate (variable), indeterminates (also called variable (mathematics), variables) and coefficients, that involves only the operations of addit ...

size

analytic proof {{Short description, Fundamental theory of logical analysis In mathematics, an analytic proof is a proof of a theorem in analysis that only makes use of methods from analysis, and that does not predominantly make use of algebraic or geometrical meth ...

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, of three gloves, at least two must be right-handed or at least two must be l ...

is known to have only

exponential Exponential may refer to any of several mathematical topics related to exponentiation, including: * Exponential function, also: **Matrix exponential, the matrix analogue to the above *Exponential decay, decrease at a rate proportional to value * Ex ...

size proofs.A. Haken, �
The intractability of resolution
��.

Theoretical Computer Science Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation. It is difficult to circumscribe the theoretical areas precisely. The Associati ...

39 (1985), pp. 297–308.

References

External links

*{{Commons category-inline Logical calculi Proof theory Logical expressions Non-classical logic

Overview

References

Further reading

External links