Planar and braided proof-nets for multiplicative linear logic with mix

Archive for Mathematical Logic 37 (5-6):309-325 (1998)
  Copy   BIBTEX


We consider a class of graphs embedded in $R^2$ as noncommutative proof-nets with an explicit exchange rule. We give two characterization of such proof-nets, one representing proof-nets as CW-complexes in a two-dimensional disc, the other extending a characterization by Asperti. As a corollary, we obtain that the test of correctness in the case of planar graphs is linear in the size of the data. Braided proof-nets are proof-nets for multiplicative linear logic with Mix embedded in $R^3$ . In order to prove the cut-elimination theorem, we consider proof-nets in $R^2$ as projections of braided proof-nets under regular isotopy.



    Upload a copy of this work     Papers currently archived: 84,179

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

A new correctness criterion for cyclic proof nets.V. Michele Abrusci & Elena Maringelli - 1998 - Journal of Logic, Language and Information 7 (4):449-459.
Completeness of MLL Proof-Nets w.r.t. Weak Distributivity.Jean-Baptiste Joinet - 2007 - Journal of Symbolic Logic 72 (1):159 - 170.
Interpolation in fragments of classical linear logic.Dirk Roorda - 1994 - Journal of Symbolic Logic 59 (2):419-444.
Homology of proof-nets.François Métayer - 1994 - Archive for Mathematical Logic 33 (3):169-188.
Modularity of proof-nets.Roberto Maieli & Quintijn Puite - 2005 - Archive for Mathematical Logic 44 (2):167-193.
Proof nets and the complexity of processing center embedded constructions.Mark Johnson - 1998 - Journal of Logic, Language and Information 7 (4):433-447.
On the Jordan-Hölder decomposition of proof nets.Quintijn Puite & Harold Schellinx - 1997 - Archive for Mathematical Logic 37 (1):59-65.
Advances in linear logic.Jean-Yves Girard, Yves Lafont & Laurent Regnier (eds.) - 1995 - New York, NY, USA: Cambridge University Press.


Added to PP

39 (#325,142)

6 months
1 (#510,113)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Gianluigi Bellin
Università degli Studi di Verona

Citations of this work

A geometrical procedure for computing relaxation.Gabriele Pulcini - 2009 - Annals of Pure and Applied Logic 158 (1-2):80-89.

Add more citations

References found in this work

Quantales and (noncommutative) linear logic.David N. Yetter - 1990 - Journal of Symbolic Logic 55 (1):41-64.

Add more references