pith. sign in

arxiv: 1609.04693 · v1 · pith:T7KD2U4Anew · submitted 2016-09-15 · 💻 cs.LO

MALL proof nets identify proofs modulo rule commutation

classification 💻 cs.LO
keywords ruleproofproofscommutationcut-freeidentifymallmodulo
0
0 comments X
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.