Resource Management for the Inverse Method in Linear Logic

One central aspect of proof search in linear logic is resource management. Strategies for efficient resource management have been developed for backward-directed calculi, such as top-down linear logic programming, tableaux calculi, and matrix methods. In this paper we consider resource management for forward-directed calculi, such as the inverse method, clausal resolution, and bottom-up linear logic programming. We focus on the inverse method for intuitionistic linear logic, and isolate the resource management problems. They turn out to come from exponentials, additive unit, and multiplicative unit, exhibiting some surprising differences from the backward-directed calculi. Our solution employs controlled contraction and weakening, and introduces affine hypotheses into sequents.