## Logic Programming in a Fragment of Intuitionistic Linear Logic:
Extended Abstract

**Joshua S Hodas and Dale Miller**
*Abstract:* Logic programming languages based on fragments
of intuitionistic logic have recently been developed and studied by
several researchers In such languages, implications are permitted
in goals and in the bodies of clauses. Attempting to prove a goal
of the form *D* \supset *G* in a context Gamma leads to
an attempt to prove the goal *G* in the extended context Gamma
\cup {*D*}. While an intuitionistic notion of context has many
uses, it has turned out to be either too powerful or too limiting
in several settings. We refine the intuitionistic notion of context
by using a fragment of Girard's linear logic that includes additive
and multiplicative conjunction, linear implication, universal
quantification, the ``of course'' exponential, and the constants 1
(the empty context) and T (for ``erasing'' contexts). After
presenting our fragment of linear logic, we show that the logic has
a goal-directed interpretation. We also show that the
non-determinism that results from the need to split contexts in
order to prove a multiplicative conjunction can be handled by
viewing proof search as a process that takes a context, consumes
part of it, and returns the rest (to be consumed elsewhere).
Examples taken from theorem proving, natural language parsing, and
data base programming are presented: each example requires a
linear, rather than intuitionistic, notion of context to be modeled
adequately.

*LFCS report ECS-LFCS-91-158*

A revised version
appeared the *Journal of Information and Computation*,
110(2):327-365, 1 May 1994.

Previous |

Index |

Next