From Proof nets to the Free *-Autonomous Categories - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Logical Methods in Computer Science Année : 2004

From Proof nets to the Free *-Autonomous Categories

Résumé

In the first part of this paper we present a theory of proof nets for full multiplicative linear logic, including the two 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 show the standard results of sequentialization and strong normalization of cut elimination. In the second part of the paper we show that the identifications enforced on proofs are such that the class of two-conclusion proof nets defines the free *-autonomous category.
Fichier principal
Vignette du fichier
From_proof_nets_to_the_free_autonomous_category.pdf (2.12 Mo) Télécharger le fichier

Dates et versions

inria-00099865 , version 1 (15-11-2006)
inria-00099865 , version 2 (16-11-2006)

Identifiants

Citer

Francois Lamarche, Lutz Strassburger. From Proof nets to the Free *-Autonomous Categories. [Research Report] A04-R-390 || lamarche04a, 2004, 45 p. ⟨inria-00099865v1⟩
106 Consultations
227 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More