We present a syntax for MALL (multiplicative additive linear logic without units) proof nets which refines Girard’s one. It is also based on the use of monomial weights for identifying additive components (slices). Our generaliza- tion gives the possibility of representing a kind of sharing of nodes which does not exist in Girard’s nets. This sharing leads to the definition of a strong cut elimination procedure for MALL. We give a correctness criterion which is proved to be sta- ble by reduction and to give a sequentialization theorem with respect to the sequent calculus. Sequentialization is proved by showing that an expansion procedure allows us to unfold any of our proof nets into a Girard proof net.
Maieli, R., Laurent, O. (2008). Cut Elimination for Monomial MALL Proof Nets. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008) (pp.486-497). IEEE Computer Society [10.1109/LICS.2008.31].
Cut Elimination for Monomial MALL Proof Nets
MAIELI, ROBERTO;
2008-01-01
Abstract
We present a syntax for MALL (multiplicative additive linear logic without units) proof nets which refines Girard’s one. It is also based on the use of monomial weights for identifying additive components (slices). Our generaliza- tion gives the possibility of representing a kind of sharing of nodes which does not exist in Girard’s nets. This sharing leads to the definition of a strong cut elimination procedure for MALL. We give a correctness criterion which is proved to be sta- ble by reduction and to give a sequentialization theorem with respect to the sequent calculus. Sequentialization is proved by showing that an expansion procedure allows us to unfold any of our proof nets into a Girard proof net.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
