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