Skip Navigation


Journal of Logic and Computation Advance Access originally published online on September 5, 2008
Journal of Logic and Computation 2009 19(2):323-339; doi:10.1093/logcom/exn054
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Jerábek, E.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

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

Original Articles

Proof Complexity of the Cut-free Calculus of Structures

Emil Jerábek

Institute of Mathematics of the Academy of Sciences, Zitná 25, 115 67 Praha 1, Czech Republic.

E-mail: jerabek{at}math.cas.cz

Received 26 November 2007.

We investigate the proof complexity of analytic subsystems of the deep inference proof system SKSg (the calculus of structures). Exploiting the fact that the cut rule (i{uparrow}) of SKSg corresponds to the ¬-left rule in the sequent calculus, we establish that the ‘analytic'system KSg+c{uparrow} has essentially the same complexity as the monotone Gentzen calculus MLK. In particular, KSg+c{uparrow} quasipolynomially simulates SKSg, and admits polynomial-size proofs of some variants of the pigeonhole principle.

Keywords: proof complexity; calculus of structures; monotone sequent calculus; cut rule



References

  1. Atserias A, Galesi N, Pudlák P. Monotone simulations of non-monotone proofs. Journal of Computer and System Sciences (2002) 65:626–638.[CrossRef][Web of Science]
  2. Bonet ML, Pitassi T, Raz R. No feasible interpolation for TC0-Frege proofs. (1997) Washington, DC. IEEE Computer Society. 254–263. In Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science.
  3. Brünnler K. Deep Inference and Symmetry in Classical Proofs (2004) Berlin: Logos Verlag.
  4. Brünnler K. Deep Inference and its Normal Form of Derivations. Beckmann A, Berger U, Löwe B, Tucker JV, eds. (2006) Springer, Heidelberg. 65–74. In Logical Approaches to Computational Barriers, Proceedings of the 2nd Conference on Computability in Europe, CiE 2006, Vol. 3988 of Lecture Notes on Computer Science.
  5. Bruscoli P, Guglielmi A. On the proof complexity of deep inference. ACM Transactions on Computational Logic (2008) (to appear).
  6. Bruscoli P, Guglielmi A. On analytic inference rules in the calculus of structures. (2007) Last accessed on 22 August 2008. Available at http://cs.bath.ac.uk/ag/p/Onan.pdf.
  7. Buss SR. Polynomial size proofs of the propositional pigeonhole principle. Journal of Symbolic Logic (1987) 52:916–927.[CrossRef][Web of Science]
  8. Cook SA, Reckhow RA. The relative efficiency of propositional proof systems. Journal of Symbolic Logic (1979) 44:36–50.[CrossRef][Web of Science]
  9. Guglielmi A. Asystem of interaction and structure. ACMTransactions on Computational Logic (2007) 8:1–64.[CrossRef]
  10. Guglielmi A, Straßburger L. Non-commutativity and MELL in the calculus of structures. Fribourg L, ed. (2001) Springer, Heidelberg. 54–68. In Proceedings of the Computer Science Logic: 15th International Workshop, CSL 2001, Vol. 2142 of Lecture Notes in Computer Science.
  11. Krajícek J. Lower bounds to the size of constant-depth propositional proofs. Journal of Symbolic Logic (1994) 59:73–86.[CrossRef][Web of Science]
  12. Krajícek J. Bounded arithmetic, propositional logic, and complexity theory (1995) 60. Cambridge: Cambridge University Press. Encyclopedia of Mathematics and Its Applications.
  13. McKinley R. Classical categories and deep inference. In. In: Structures and Deduction – the Quest for the Essence of Proofs (satellite workshop of ICALP 2005)—Bruscoli P, Lamarche F, Stewart C, eds. (2005) Dresden: Technische Universität Dresden. 19–33.

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



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Jerábek, E.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?