The inverse method for intuitionistic linear logic : (the propositional fragment)

Abstract: "We present a forward sequent calculus for intuitionistic propositional linear logic ([circle with x], 1, &, T, -o, [circle with plus], 0, !) and a corresponding inverse-method search strategy. Our approach centres around resource management, inspired by similar approaches for backward-directed calculi such as top-down linear logic programming. Surprisingly, the resource management problems for the forward direction turn out to have a different character to those of the backward direction, arising for different connectives. Our approach identifies conditions for which we may relax linearity to allowing (implicit) weakening. We characterize two such classes of affine behaviour -- as a form of weak sequent designed to handle T-weakening lazily, and as affine contexts to control the multiplicative unit 1 using a general matching framework."