Planar and Braided Proof-nets for MLL with Mix

MR1634276 (99m:03120) The authors consider representations of proofs as graphs for the multiplicative fragment of linear logic with the mix-rule in the planar and braided cases. They give two interesting characterizations of planar representations of proofs, one representing proof-nets as CW-complexes in a two-dimensional disc, the other extending Asperti's characterization of proofs as concurrent processes. In order to prove the cut-elimination theorem, the authors consider planar proof-nets as projections of three-dimensional objects, braided proof-nets under regular isotopy. (Reviewed by R. Gylys) Cited by: Métayer, F. Implicit exchange in multiplicative proofnets. Math. Struct. Comput. Sci. 11, No.2, 261-272 (2001). Gaubert, C.Two-dimensional proof-structures and the exchange rule. [Math. Struct. Comput. Sci. 14, No. 1, 73-96 (2004) Andreoli J-M; Pulcini G. ; Ruet P. Permutative logic: a geometrical study on linear logic proofs, Computer Science Logic. Springer. LNCS 3634: 184-199, 2005 G.Pulcini. Permutative Additives and Exponentials, In: Logic for Programming, Artificial Intelligence, and Reasoning, Springer Lecture Notes in Computer Science Vol. 4790, 2007