Abstract
The sequent calculus admits many proofs of the same conclusion that differ only by trivial permutations of inference rules. In order to eliminate this “bureaucracy” from sequent proofs, deductive formalisms such as proof nets or natural deduction are usually used instead of the sequent calculus, for they identify proofs more abstractly and geometrically. In this paper we recover permutative canonicity directly in the cut-free sequent calculus by generalizing focused sequent proofs to admit multiple foci, and then considering the restricted class of maximally multi-focused proofs. We validate this definition by proving a bijection to the well-known proof-nets for the unit-free multiplicative linear logic, and discuss the possibility of a similar correspondence for larger fragments.
Chapter PDF
Similar content being viewed by others
References
J.-M. Andreoli and R. Maieli. Focusing and proof nets in linear and noncommutative logic. In International Conference on Logic for Programming and Automated Reasoning (LPAR), volume 1581 of LNAI. Springer, 1999.
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. of Logic and Computation, 2(3):297–347, 1992.
Jean-Marc Andreoli. Focussing proof-net construction as a middleware paradigm. In Andrei Voronkov, editor, 18th Conference on Automated Deduction (CADE), number 2392 in LNAI, pages 501–516. Springer, 2002.
Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. J. of Automated Reasoning, 40(2-3):133–177, March 2008.
Pierre-Louis Curien. Introduction to linear logic and ludics, Part I. Advances in Mathitatics (China), 34(5):513–544, January 2005.
Pierre-Louis Curien and Claudia Faggian. L-nets, strategies and proof-nets. In C.-H. Luke Ong, editor, CSL 2005: Computer Science Logic, volume 3634 of LNCS, pages 167–183. Springer, 2005.
Olivier Delande and Dale Miller. A neutral approach to proof and refutation in MALL. In F. Pfenning, editor, 23th Symp. on Logic in Computer Science. IEEE Computer Society Press, 2008.
Claudia Faggian and François Maurel. Ludics nets, a game model of concurrent interaction. In 20th Symp. on Logic in Computer Science, pages 376–385. IEEE Computer Society, 2005.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
Jean-Yves Girard. Proof-nets: the parallel syntax for proof-theory. In Aldo Ursini and Paolo Agliano, editors, Logic and Algebra, volume 180 of Lecture Notes In Pure and Applied Mathitatics, pages 97–124, New York, 1996. Marcel Dekker.
Jean-Yves Girard. Locus solum. Mathitatical Structures in Computer Science, 11(3):301–506, June 2001.
Dominic Hughes and Rob Van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic. ACM Trans. on Computational Logic, 6:784–842, 2005.
Stephen Cole Kleene. Permutabilities of inferences in Gentzen’s calculi LK and LJ. Mitoirs of the American Mathitatical Society, 10:1–26, 1952.
François Lamarche and Lutz Straβburger. From proof nets to the free *-autonomous category. Logical Methods in Computer Science, 2(4:3):1–44, 2006.
Chuck Liang and Dale Miller. Focusing and polarization in intuitionistic logic. In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 451–465. Springer, 2007.
Dale Miller and Alexis Saurin. From proofs to focused proofs: a modular proof of focalization in linear logic. In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 405–419. Springer, 2007.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Chaudhuri, K., Miller, D., Saurin, A. (2008). Canonical Sequent Proofs via Multi-Focusing. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds) Fifth Ifip International Conference On Theoretical Computer Science – Tcs 2008. IFIP International Federation for Information Processing, vol 273. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-09680-3_26
Download citation
DOI: https://doi.org/10.1007/978-0-387-09680-3_26
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-09679-7
Online ISBN: 978-0-387-09680-3
eBook Packages: Computer ScienceComputer Science (R0)