## The Uniform Proof-Theoretic Foundation of Linear Logic
Programming

**James Harland and David Pym**
*Abstract:* We present a theory of *logic programming*
for Girard's *linear logic*. In the spirit of recent work of
Miller *et al*., we identify suitable classes of *definite
formulae* and *goal formulae* by considering classes of
formulae that resemble the Harrop formulae of intuitionistic
first-order logic. We isolate the appropriate notion of *uniform
proof* in linear logic, and show that this characterizes
*resolution* proofs. 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 clause
selected to be *deleted* after use.

We provide an elementary *quantale semantics* for our logic
programs and give an appropriate *completeness theorem*.

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

*LFCS report ECS-LFCS-90-124*

Previous |

Index |

Next