“Cirquent calculus”的意思、由来-开放百科全书

Cirquent calculus is a proof calculus which 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).

Among the later-found applications of cirquent calculus was the use of it to define a semantics for purely propositional independence-friendly logic.^[6] The corresponding logic was axiomatized by W. Xu.^[7]

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.^[8] Only quasipolynomial analytic proofs have been found for this principle in other deep inference systems.^[9] In resolution or analytic Gentzen-style systems, the pigeonhole principle is known to have only exponential size proofs.^[10]

Literature

References

1. ^G.Japaridze, “Introduction to cirquent calculus and abstract resource semantics”. Journal of Logic and Computation 16 (2006), pp. 489–532.
2. ^G.Japaridze, “[https://link.springer.com/article/10.1007/s00153-012-0313-8 The taming of recurrences in computability logic through cirquent calculus, Part I]”.Archive for Mathematical Logic 52 (2013), pages 173-212.
3. ^ G.Japaridze, [https://link.springer.com/article/10.1007/s00153-012-0314-7 “The taming of recurrences in computability logic through cirquent calculus, Part II]” Archive for Mathematical Logic 52 (2013), pages 213–259.
4. ^G.Japaridze, "Introduction to cirquent calculus and abstract resource semantics". Journal of Logic and Computation 16 (2006), pp. 489–532.
5. ^G.Japaridze, “Cirquent calculus deepened.” Journal of Logic and Computation 18 (2008), pp. 983–1028.
6. ^ G.Japaridze, “From formulas to cirquents in computability logic”. Logical Methods is Computer Science 7 (2011), Issue 2 , Paper 1, pp. 1–55.
7. ^W.Xu, “A propositional system induced by Japaridze's approach to IF logic”. Logic Journal of the IGPL 22 (2014), pages 982–991.
8. ^G.Japaridze, “Cirquent calculus deepened.” Journal of Logic and Computation 18 (2008), pp. 983–1028.
9. ^A. Das, “On the pigeonhole and related principles in Deep inference and monotone systems”.
10. ^A. Haken, “The intractability of resolution”. Theoretical Computer Science 39 (1985), pp. 297-308.