Complexity in propositional substructural logics and counter systems

Sylvain Schmitz

The ties between propositional linear logic on the one hand and extensions of vector addition systems on the other hand have long been known, as they lie for instance at the heart of Lincoln et al.'s 1992 undecidability proof. With Ranko Lazić we recently revisited these connections with an eye on complexity issues, which allowed us to prove tight complexity bounds on provability in affine and contractive fragments of linear logic. Our work also yields a new Tower lower bound on provability in MELL, for which decidability is still open.

Joint work with Ranko Lazić presented at CSL-LICS 2014; full paper to appear in ToCL and available at