Journal of Logic and Computation

Journal of Logic and Computation Advance Access originally published online on July 21, 2008
Journal of Logic and Computation 2008 18(6):983-1028; doi:10.1093/logcom/exn019

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Similar articles in ISI Web of Science Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Search for citing articles in: ISI Web of Science (1) Request Permissions Google Scholar Articles by Japaridze, G. Search for Related Content Social Bookmarking          What's this?

© The Author, 2008. Published by Oxford University Press. All rights reserved. for Permissions, please email: journals.permissions@oxfordjournals.org

Original Articles

Cirquent Calculus Deepened

Giorgi Japaridze

Institute of Artificial Intelligence, Xiamen University, China; Department of Computing Sciences, Villanova University, USA.

E-mail: giorgi.japaridze{at}villanova.edu

Received 10 September 2007.

Cirquent calculus is a new proof-theoretic and semantic framework, whose main distinguishing feature is being based on circuit-style structures (called cirquents), as opposed to the more traditional approaches that deal with tree-like objects such as formulas, sequents or hypersequents. Among its advantages are greater efficiency, flexibility and expressiveness. This article presents a detailed elaboration of a deep-inference cirquent logic, which is naturally and inherently resource conscious. It shows that classical logic, both syntactically and semantically, can be seen to be just a special, conservative fragment of this more general and, in a sense, more basic logic—the logic of resources in the form of cirquent calculus. The reader will find various arguments in favour of switching to the new framework, such as arguments showing the insufficiency of the expressive power of linear logic or other formula-based approaches to developing resource logics, exponential improvements over the traditional approaches in both representational and proof complexities offered by cirquent calculus (including the existence of polynomial size cut-, substitution- and extension-free cirquent calculus proofs for the notoriously hard pigeonhole principle), and more. Among the main purposes of this article is to provide an introductory-style starting point for what, as the author wishes to hope, might have chances to become a new line of research in proof theory—a proof theory based on circuits instead of formulas.

Keywords: Proof theory; cirquent calculus; resource semantics; deep inference; computability logic; pigeonhole principle

References

1. Avron A. A constructive analysis of RM. Journal of Symbolic Logic (1987) 52:939–951.[CrossRef][Web of Science]
2. Blass A. A game semantics for linear logic. Annals of Pure and Applied Logic (1992) 56:183–220.[CrossRef][Web of Science]
3. Bruscoli P, Guglielmi A. On the proof complexity of deep inference. ACM Transactions on Computational Logic. in press.
4. Brünnler K. Deep Inference and Symmetry in Classical Proofs (2004) Berlin: Logos Verlag.
5. Buss S. Polynomial size proofs of the propositional pigeonhole principle. Journal of Symbolic Logic (1987) 52:916–927.[CrossRef][Web of Science]
6. Cook S, Rechkow R. The relative efficiency of propositional proof systems. Journal of Symbolic Logic (1979) 44:36–50.[CrossRef][Web of Science]
7. Finger M. DAG sequent proofs with a substitution rule. In: We Will Show Them — Essays in Honor of Dov Gabbay's 60th Birthday (2005) London: Kings College Publications. 671–686.
8. Gordeev L, Haeusler EH, da Costa VG. Proof compressions with circuit-structured substitutions. (2007).
9. Guglielmi A, Strassburger L. Non-commutativity and MELL in the calculus of structures (2001) Paris: Computer Science Logic. 54–68. Vol. 2142 of Lecture Notes in Computer Science, Springer, Berlin, 2001.
10. Guglielmi A. Asystem of interaction and structure. ACMTransactions on Computational Logic (2007) 8:1–64.[CrossRef]
11. Haken A. The intractability of resolution. Theoretical Computer Science (1985) 39:297–308.[CrossRef][Web of Science]
12. Japaridze G. Introduction to computability logic. Annals of Pure and Applied Logic (2003) 123:1–99.[CrossRef][Web of Science]
13. Japaridze G. Computability logic: a formal theory of interaction. In: Interactive Computation: The New Paradigm—Goldin D, Smolka S, Wegner P, eds. (2006) Berlin: Springer Verlag. 182–223.
14. Japaridze G. Introduction to cirquent calculus and abstract resource semantics. Journal of Logic and Computation (2006) 16:489–532.[Abstract/Free Full Text]
15. Japaridze G. In the beginning was game semantics. In: Games: Unifying Logic, Language and Philosophy—Majer O, Pietarinen A-V, Tulenheimo T, eds. (in press) Berlin: Springer Verlag.
16. Japaridze G. Sequential operators in computability logic. Available at http://arxiv.org/abs/0712.1345.
17. Pottinger G. Uniform, cut-free formulations of T, S4 and S5 (abstract). Journal of Symbolic Logic (1983) 48:900.

CiteULike    Connotea    Del.icio.us    What's this?

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Similar articles in ISI Web of Science Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Search for citing articles in: ISI Web of Science (1) Request Permissions Google Scholar Articles by Japaridze, G. Search for Related Content Social Bookmarking          What's this?