file.pdf (213.91 kB)
Resource Management for the Inverse Method in Linear Logic
journal contribution
posted on 2004-01-01, 00:00 authored by Kaustuv Chaudhuri, Frank PfenningOne 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.