Polarized Proof-Nets: Proof-Nets for LC
Laurent, Olivier
HAL, hal-00009136 / Harvested from HAL
We define a notion of polarization in linear logic (LL) coming from the polarities of Jean-Yves Girard's classical sequent calculus LC. This allows us to define a translation between the two systems. Then we study the application of this polarization constraint to proof-nets for full linear logic. 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.
Publié le : 1999-07-05
Classification:  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO]
@article{hal-00009136,
     author = {Laurent, Olivier},
     title = {Polarized Proof-Nets: Proof-Nets for LC},
     journal = {HAL},
     volume = {1999},
     number = {0},
     year = {1999},
     language = {en},
     url = {http://dml.mathdoc.fr/item/hal-00009136}
}
Laurent, Olivier. Polarized Proof-Nets: Proof-Nets for LC. HAL, Tome 1999 (1999) no. 0, . http://gdmltest.u-ga.fr/item/hal-00009136/