Abstract

We consider a class of graphs embedded in $R^2$ as noncommutative proof-nets with an explicit exchange rule. We give two characterization of such proof-nets, one representing proof-nets as CW-complexes in a two-dimensional disc, the other extending a characterization by Asperti. As a corollary, we obtain that the test of correctness in the case of planar graphs is linear in the size of the data. Braided proof-nets are proof-nets for multiplicative linear logic with Mix embedded in $R^3$ . In order to prove the cut-elimination theorem, we consider proof-nets in $R^2$ as projections of braided proof-nets under regular isotopy.