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 (obtained by mutilating one premise of each disjunction link) can be naturally viewed as a series-parallel order variety (a cyclic relation) on the conclusions of the proof net.
Maieli, R. (2003). A new correctness criterion for multiplicative non commutative proof-nets. ARCHIVE FOR MATHEMATICAL LOGIC, 42(3), 205-220 [10.1007/s001530100127].
A new correctness criterion for multiplicative non commutative proof-nets
MAIELI, ROBERTO
2003-01-01
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 (obtained by mutilating one premise of each disjunction link) can be naturally viewed as a series-parallel order variety (a cyclic relation) on the conclusions of the proof net.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
