Hal will be stopped for maintenance from friday on june 10 at 4pm until monday june 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

On Proof Nets for Multiplicative Linear Logic with Units

Lutz Strassburger 1 François Lamarche 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper a theory of proof nets for multiplicative linear logic is presented, which includes the two multiplicative units. It naturally extends the well-known theory of unit-free multiplicative proof nets: A linking is no longer a set of axiom links but a tree in which the axiom links are subtrees. These trees will be identified according to an equivalence relation based on a simple form of graph rewriting. We will have the standard results of sequentialisation and strong normalisation of cut elimination. Furthermore, the identifications enforced on proofs are such that the proof nets, as they are presented here, form the arrows of the free (symmetric) *-autonomous category.
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 10:16:04 AM
Last modification on : Friday, February 4, 2022 - 3:30:50 AM


  • HAL Id : inria-00100244, version 1



Lutz Strassburger, François Lamarche. On Proof Nets for Multiplicative Linear Logic with Units. 18th International Workshop on Computer Science Logic - CSL'2004, 2004, Karpacz, Poland, pp.145--159. ⟨inria-00100244⟩



Record views