Abstract
We define a notion of polarization in linear logic (LL) coming from the polarities of Jean-Yves Girard’s classical sequent calculus LC [4]. This allows us to define a translation between the two systems. Then we study the application of this polar ization constraint to proofnets for full linear logic described in [7]. This yields an important simplification of the correctness criterion for polarized proof-nets. In this way we obtain a system of proof-nets for LC.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. Computational isomorphisms in classical logic (extended abstract). In Jean-Yves Girard, Mitsu Okada, and Andr Scedrov, editors, Proceedings Linear Logic’ 96 Tokyo Meeting, volume 3 of Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam, 1996.
Vincent Danos and Laurent Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181–203, 1989.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
Jean-Yves Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1(3):255–296, 1991.
Jean-Yves Girard. Quantifiers in linear logic II. In Corsi and Sambin, editors, Nuovi problemi della logica e della filosofia della scienza, pages 79–90, Bologna, 1991. CLUEB.
Jean-Yves Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201–217, 1993.
Jean-Yves Girard. Proof-nets: the parallel syntax for proof-theory. In Ursini and Agliano, editors, Logic and Algebra, New York, 1996. Marcel Dekker.
Franois Lamarche. From proof nets to games (extended abstract). In Jean-Yves Girard, Mitsu Okada, and Andr Scedrov, editors, Proceedings Linear Logic’ 96 Tokyo Meeting, volume 3 of Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam, 1996.
Myriam Quatrini and Lorenzo Tortora de Falco. Polarisation des preuves classiques et renversement. Compte Rendu de l’Acadmie des Sciences de Paris, 323:113–116, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Laurent, O. (1999). Polarized Proof-Nets: Proof-Nets for LC. In: Girard, JY. (eds) Typed Lambda Calculi and Applications. TLCA 1999. Lecture Notes in Computer Science, vol 1581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48959-2_16
Download citation
DOI: https://doi.org/10.1007/3-540-48959-2_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65763-7
Online ISBN: 978-3-540-48959-7
eBook Packages: Springer Book Archive