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.
Type de document :
Communication dans un congrès
Jerzy Marcinkowski and Andrzej Tarlecki. 18th International Workshop on Computer Science Logic - CSL'2004, 2004, Karpacz, Poland, Springer-Verlag, 3210, pp.145--159, 2004, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00100244
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:16:04
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00100244, version 1

Collections

Citation

Lutz Strassburger, François Lamarche. On Proof Nets for Multiplicative Linear Logic with Units. Jerzy Marcinkowski and Andrzej Tarlecki. 18th International Workshop on Computer Science Logic - CSL'2004, 2004, Karpacz, Poland, Springer-Verlag, 3210, pp.145--159, 2004, Lecture Notes in Computer Science. 〈inria-00100244〉

Partager

Métriques

Consultations de la notice

118