MALL proof nets identify proofs modulo rule commutation
Logic in Computer Science
2016-09-16 v1
Abstract
We show that the proof nets introduced in [Hughes & van Glabbeek 2003, 2005] for MALL (Multiplicative Additive Linear Logic, without units) identify cut-free proofs modulo rule commutation: two cut-free proofs translate to the same proof net if and only if one can be obtained from the other by a succession of rule commutations. This result holds with and without the mix rule, and we extend it with cut.
Keywords
Cite
@article{arxiv.1609.04693,
title = {MALL proof nets identify proofs modulo rule commutation},
author = {Rob van Glabbeek and Dominic Hughes},
journal= {arXiv preprint arXiv:1609.04693},
year = {2016}
}