From Proof Nets to the Free *-Autonomous Category
arXiv:cs/0605054 · doi:10.2168/LMCS-2(4:3)2006
Abstract
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.
LaTeX, 44 pages, final version for LMCS; v2: updated bibliography
References in corpus (4)
Cited by in corpus (8)
- Normalisation Control in Deep Inference via Atomic Flows
- A System of Interaction and Structure IV: The Exponentials and Decomposition
- Proof equivalence in MLL is PSPACE-complete
- Coherence for Frobenius pseudomonoids and the geometry of linear proofs
- Graphical Presentations of Symmetric Monoidal Closed Theories
- Binding bigraphs as symmetric monoidal closed theories
- Constructing Fully Complete Models of Multiplicative Linear Logic
- Proof Nets, Coends and the Yoneda Isomorphism