Case study: Additive linear logic and lattices

Abstract

We investigate sequent calculus where contexts, called additive contexts, are governed by the operations of a non-distributive lattice. We present a sequent calculus ALL _m with multiple antecedents and succedents. ALL _m is complete for non-distributive lattices and is equivalent to the additive fragment of linear logic. Weakenings and contractions are postulated for ALL _m and cut is redundant. We extend this construction in order to get a sequent calculus for propositional linear logic with both additive and multiplicative contexts.

Then we show that a bottom-up decision procedure based on the cut-free sequent calculi runs in exponential time. We provide a decision algorithm that exploits analytic cuts and whose runtime is polynomial.