Cirquent calculus
Cirquent calculus is a proof calculus that manipulates graph-style constructs termed cirquents, as opposed to the traditional tree-style objects such as formulas or sequents. 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
[edit]The approach was introduced by G. Japaridze[1] as an alternative proof theory capable of "taming" various nontrivial fragments of his computability logic, which had otherwise resisted all axiomatization attempts within the traditional proof-theoretic frameworks.[2][3] 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 sequents (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[1] 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. 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.[4]
The resource philosophy of cirquent calculus sees the approaches of linear logic and classical logic 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.[5] The corresponding logic was axiomatized by W. Xu.[6]
Syntactically, cirquent calculi are deep inference systems with the unique feature of subformula-sharing. This feature has been shown to provide speedup for certain proofs. For instance, polynomial size analytic proofs for the propositional pigeonhole have been constructed.[4] Only quasipolynomial analytic proofs have been found for this principle in other deep inference systems.[7] In resolution or analytic Gentzen-style systems, the pigeonhole principle is known to have only exponential size proofs.[8]
References
[edit]- ^ a b G.Japaridze, “Introduction to cirquent calculus and abstract resource semantics”. Journal of Logic and Computation 16 (2006), pp. 489–532.
- ^ 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.
- ^ a b Japaridze, Giorgi (2008), "Cirquent calculus deepened", Journal of Logic and Computation, 18 (6): 983–1028, arXiv:0709.1308, doi:10.1093/logcom/exn019, MR 2460926
- ^ G.Japaridze, “From formulas to cirquents in computability logic”. Logical Methods in Computer Science 7 (2011), Issue 2, Paper 1, pp. 1–55.
- ^ Xu, Wenyan (2014), "A propositional system induced by Japaridze's approach to IF logic", Logic Journal of the IGPL, 22 (6): 982–991, arXiv:1402.4172, doi:10.1093/jigpal/jzu020, MR 3285333
- ^ A. Das, “On the pigeonhole and related principles in Deep inference and monotone systems”.
- ^ A. Haken, “The intractability of resolution”. Theoretical Computer Science 39 (1985), pp. 297–308.
Further reading
[edit]- M.Bauer, “The computational complexity of propositional cirquent calculus”. Logical Methods in Computer Science 11 (2015), Issue 1, Paper 12, pp. 1–16.
- 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 cirquent calculus system with clustering and ranking. Journal of Applied Logic 16 (2016), pp. 37–49.
External links
[edit]
Media related to Cirquent calculus at Wikimedia Commons
