## The Uniform Proof-theoretic Foundation of Linear Logic
Programming (Extended Abstract)

**James Harland and David Pym**
*Abstract:* We present a proof-theoretic analysis of a
natural notion of *logic programming* for Girard's *linear
logic*. This analysis enables us to identify a suitable notion
of *uniform proof*. This in turn enables us to identify
choices of classes of definite and goal formulae for which uniform
proofs are complete and so to obtain the appropriate formulation of
*resolution proof* for such choices. Resolution proofs in
linear logic are somewhat difficult to define. This difficulty
arises from the need to decompose definite formulae into a form
suitable for the use of the linear resolution rule, a rule which
requires the selected clause to be *deleted* after use, and
from the presence of the *modality*! (of course).

We consider a *translation* - resembling those of Girard -
of the intuitionistic hereditary Harrop formulae and
inntuitionistic uniform proofs into our framework, and show that
certain properties are preserved under this translation.

We sketch the design of an *interpreter* for linear logic
programs.

*LFCS report ECS-LFCS-91-168*

Previous |

Index |

Next