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 metadatas

https://hal.inria.fr/inria-00100244
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 10:16:04 AM
Last modification on : Thursday, January 11, 2018 - 6:19:48 AM

Identifiers

  • HAL Id : inria-00100244, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

186