MALL proof nets identify proofs modulo rule commutation
classification
💻 cs.LO
keywords
ruleproofproofscommutationcut-freeidentifymallmodulo
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.