Skip Navigation



Journal of Logic and Computation Advance Access published online on August 10, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp047
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 Strassburger, L.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

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

Original Papers

From Deep Inference to Proof Nets via Cut Elimination

Lutz Strassburger

INRIA Saclay–Île-de-France, France; École Polytechnique, LIX, Rue de Saclay, 91128 Palaiseau Cedex, France.
E-mail: lutz{at}lix.polytechnique.fr

Received 11 February 2009.

This article shows how derivations in the deep inference system SKS for classical propositional logic can be translated into proof nets. Since an SKS derivation contains more information about a proof than the corresponding proof net, we observe a loss of information which can be understood as ‘eliminating bureaucracy’. Technically, this is achieved by cut reduction on proof nets. As an intermediate step between the two extremes, SKS derivations and proof nets, we will see proof graphs representing derivations in ‘Formalism A’.

Keywords: Classical propositional logic; deep inference; proof nets; atomic flows; cut elimination



References

  1. Bruscoli P, Guglielmi A. On the proof complexity of deep inference. ACM Transactions on Computational Logic (2009) 10:1–34.
  2. Barr M, Wells C. Category Theory for Computing Science (1999) 3rd edn. Les Publications CRM.
  3. Brünnler K. Atomic cut elimination for classical logic. In: CSL 2003—Baaz M, Makowsky JA, eds. (2003) Springer. 86–97. Vol. 2803 of Lecture Notes in Computer Science.
  4. Brünnler K. Deep Inference and Symmetry for Classical Proofs (2003) Dresden, Germany: Technische Universität Dresden. PhD Thesis.
  5. Brünnler K. (2003) Minimal logic in the calculus of structures, Note.
  6. Brünnler K. Deep sequent systems for modal logic. In: Advances in Modal Logic—Governatori G, Hodkinson I, Venema Y, eds. (2006) 6. College Publications. 107–119.
  7. Brünnler K. Locality for classical logic. Notre Dame Journal of Formal Logic (2006) 47:557–580.[CrossRef]
  8. Brünnler K, Straßburger L. Modular sequent systems for modal logic. In. Proceedings of Tableaux’09 (2009).
  9. Brünnler K, Lengrand S. On two forms of bureaucracy in derivations. In: Structures and Deduction 2005 (SatelliteWorkshop of ICALP’05)—Bruscoli P, Lamarche F, eds. (2005) Germany: Dresden.
  10. Brünnler K, Tiu AF. A local system for classical logic. In: Logic for Programming, Artificial Intelligence, and Reasoning 2001—Nieuwenhuis R, Voronkov A, eds. (2001) Springer. 347–361. Vol. 2250 of Lecture Notes in Artificial Intelligence.
  11. Buss SR. The undecidability of k-provability. Annals of Pure and Applied Logic (1991) 53:72–102.
  12. Carbone A. Interpolants, cut elimination and flow graphs for the propositional calculus. Annals of Pure and Applied Logic (1997) 83:249–299.[CrossRef][Web of Science]
  13. Cook SA, Reckhow RA. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic (1979) 44:36–50.[CrossRef]
  14. Di Gianantonio P. Structures for multiplicative cyclic linear logic: Deepness vs cyclicity. In: Computer Science Logic, CSL 2004—Marcinkowski J, Tarlecki A, eds. (2004) Springer. 130–144. Vol. 3210 of Lecture Notes in Computer Science.
  15. Dosen K, Petric Z. Proof-Theoretical Coherence (2004) KCL Publications.
  16. Führmann C, Pym D. Order-enriched categorical models of the classical sequent calculus. Journal of Pure and Applied Algebra (2004) 204:21–78.[CrossRef][Web of Science]
  17. Gentzen G. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift (1934) 39:176–210.[CrossRef][Web of Science]
  18. Girard J-Y. Linear logic. Theoretical Computer Science (1987) 50:1–102.[CrossRef][Web of Science]
  19. Girard J-Y. A new constructive logic: classical logic. Mathematical Structures in Computer Science (1991) 1:255–296.[CrossRef]
  20. Girard J-Y. Proof-nets: the parallel syntax for proof-theory. In: Logic and Algebra—Ursini A, Agliano P, eds. (1996) Marcel Dekker.
  21. Guglielmi A. (2004) Formalism A, Note.
  22. Guglielmi A. (2004) Formalism B, Note.
  23. Guglielmi A. A system of interaction and structure. ACM Transactions on Computational Logic (2007) 8:1–64.[CrossRef]
  24. Guglielmi A, Gundersen T. Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science (2008) 4:1–36.
  25. Guglielmi A, Straßburger L. A non-commutative extension of MELL. In: Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002—Baaz M, Voronkov A, eds. (2002) Springer. 231–246. Vol. 2514 of Lecture Notes in Artificial Intelligemce.
  26. Guiraud Y. The three dimensions of proofs. Annals of Pure and Applied Logic (2006) 141:266–295.[CrossRef][Web of Science]
  27. Hughes D. (2004) Deep inderence proof theory equals categorical proof theory minus coherence. preprint.
  28. Hughes D. (2005) Simple multiplicative proof nets with units. Preprint.
  29. Hughes D, van Glabbeek R. Proof nets for unit-free multiplicative-additive linear logic. (2003) 1–10. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003).
  30. Kelly GM. On MacLane's conditions for coherence of natural associativities, commutativities, etc. Journal of Algebra (1964) 4:397–402.
  31. Kelly GM, Mac Lane S. Coherence in closed categories. Journal of Pure and Applied Algebra (1971) 1:97–140.[CrossRef]
  32. Lamarche F. Exploring the gap between linear and classical logic. Theory and Applications of Categories (2007) 18:473–535.
  33. Lamarche F, Straßburger L. Constructing free Boolean categories. (2005) 209–218. In Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS’05).
  34. Lamarche F, Straßburger L. Naming proofs in classical propositional logic. In: Typed Lambda Calculi and Applications, TLCA 2005—Urzyczyn P, ed. (2005) Springer. 246–261. Vol. 3461 of Lecture Notes in Computer Science.
  35. Mac Lane S. Natural associativity and commutativity. Rice University Studies (1963) 49:28–46.
  36. Mac Lane S. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics (1971) Springer.
  37. McKinley R. Classical categories and deep inference. In: Structures and Deduction 2005 (Satellite Workshop of ICALP’05) (2005) Germany: Dresden.
  38. Robinson EP. Proof nets for classical logic. Journal of Logic and Computation (2003) 13:777–797.[Abstract/Free Full Text]
  39. Stewart C, Stouppa P. A systematic proof theory for several modal logics. In: Advances in Modal Logic—Schmidt RA, Pratt-Hartmann I, Reynolds M, Wansing H, eds. (2005) 5. King's College Publications. 309–333.
  40. Straßburger L. Alocal system for linear logic. In: Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002—Baaz M, Voronkov A, eds. (2002) Springer. 388–402. Vol. 2514 of Lecture Notes in Artificial Intelligence.
  41. Straßburger L. Linear Logic and Noncommutativity in the Calculus of Structures (2003) Dresden, Germany: Technische Universität Dresden. PhD Thesis.
  42. Straßburger L. From deep inference to proof nets. In: Structures and Deduction 2005 (Satellite Workshop of ICALP’05)—Bruscoli P, Lamarche F, eds. (2005) Germany: Dresden.
  43. Straßburger L. A characterisation of medial as rewriting rule. In: Term Rewriting and Applications, RTA’07—Baader F, ed. (2007) Springer. 344–358. Vol. 4533 of Lecture Notes in Computer Science.
  44. Straßburger L. On the axiomatisation of Boolean categories with and without medial. Theory and Applications of Categories (2007) 18:536–601.
  45. Straßburger L, Lamarche F. On proof nets for multiplicative linear logic with units. In: Computer Science Logic, CSL 2004—Marcinkowski J, Tarlecki A, eds. (2004) Springer. 145–159. Vol. 3210 of Lecture Notes in Computer Science.
  46. Stouppa P. A deep inference system for the modal logic S5. Studia Logica (2007) 85:199–214.[CrossRef]
  47. Tiu A. A local system for intuitionistic logic. In: Logic for Programming, Artificial Intelligence, and Reasoning 2006—Hermann M, Voronkov A, eds. (2006) Springer. 242–256. Vol. 4246 of Lecture Notes in Artificial Intelligence.

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 Strassburger, L.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?