Logic Programming in a Fragment of Intuitionistic Linear Logic

When logic programming is based on the proof theory of intuitionistic logic, it is natural to allow implications in goals and in the bodies of clauses. Attempting to prove a goal of the form D oe G from the context (set of formulas) \Gamma leads to an attempt to prove the goal G in the extended context \Gamma [ fDg. Thus during the bottom-up search for a cut-free proof contexts, represented as the left-hand side of intuitionistic sequents, grow as stacks. While such an intuitionistic notion of context provides for elegant specifications of many computations, contexts can be made more expressive and flexible if they are based on linear logic. After presenting two equivalent formulations of a fragment of linear logic, we show that the fragment has a goal-directed interpretation, thereby partially justifying calling it a logic programming language. Logic programs based on the intuitionistic theory of hereditary Harrop formulas can be modularly embedded into this linear logic setting. Pro..