Abstract

We introduce a new correctness criterion for multiplicative non commutative proof nets which can be considered as the non- commutative counterpart to the Danos-Regnier criterion for proof nets of linear logic. The main intuition relies on the fact that any switching for a proof net can be naturally viewed as a series-parallel order variety on the conclusions of the proof net.