Proof nets for unit-free multiplicative additive linear logic

Download files
Access & Terms of Use
open access
Abstract
A cornerstone of the theory of proof nets for unit-free multiplicative linear logic (MLL) is the abstract representation of cut-free proofs modulo inessential rule commutation. The only known extension to additives, based on monomial weights, fails to preserve this key feature: a host of cut-free monomial proof nets can correspond to the same cut-free proof. Thus, the problem of finding a satisfactory notion of proof net for unit-free multiplicative-additive linear logic (MALL) has remained open since the inception of linear logic in 1986. We present a new definition of MALL proof net which remains faithful to the cornerstone of the MLL theory.
Persistent link to this record
DOI
Additional Link
Author(s)
van Glabbeek, Robert
Hughes, Dominic
Supervisor(s)
Creator(s)
Editor(s)
Translator(s)
Curator(s)
Designer(s)
Arranger(s)
Composer(s)
Recordist(s)
Conference Proceedings Editor(s)
Other Contributor(s)
Corporate/Industry Contributor(s)
Publication Year
2005
Resource Type
Journal Article
Degree Type
UNSW Faculty
Files
download 0200506499_ProofNets.pdf 728.32 KB Adobe Portable Document Format
Related dataset(s)