Institut de Mathématiques de Luminy

Abstract 2001-13

Maieli Roberto.
A new correctness criterion for multiplicative non commutative proofs nets.

We introduce a correctness criterion for multiplicative non commutative proofs nets based on the idea of acyclic and connected graphs, which can be considered a non-commutative counterpart to the Danos-Regnier criterion for proofs nets of linear logic. The main intuition relies on the fact that a switching for a proof net can be naturally viewed as a series-parallel order variety (alga) on the conclusions of the proof net.

 

 



Last update : may 14, 2001, EL.