2016/09/15 by Rob van Glabbeek, van Glabbeek, Rob, Dominic Hughes +1
Computer Science · #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.1609.04693
arxiv created 2016/09/15 · arxiv updated 2016/09/16
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.