language: en

Efficient Resource Management for Linear Logic Proof Search

Iliano Cervesato 1 , Joshua S. Hodas 2 , and Frank Pfenning 1
1 Department of Computer Science, Carnegie Mellon University
Pittsburgh, PA 15213-3891, USA
e-mail: filianojfpg@cs.cmu.edu
2 Computer Science Department, Harvey Mudd College
Claremont, CA 91711, USA
e-mail: hodas@cs.hmc.edu

Abstract. The design of linear logic programming languages and theorem provers opens a number of new implementation challenges not present in more traditional logic languages such as Horn clauses (Prolog) and hereditary Harrop formulas (Prolog). Among these, the problem of efficiently managing the linear context when solving a goal is of crucial importance for the use of these systems in non-trivial applications. This paper studies this problem in the case of Lolli [6] (though its results have application to other systems). We first give a proof-theoretic presentation of the operational semantics of this language as a resolution calculus. We then present a series of resource management systems designed to eliminate the non-determinism in the distribution of linear formulas that undermines the efficiency of a direct implementation of this system.

[This paper will appear in the]

[proceedings of the 1996 International Workshop on Extensions of Logic Programming, Leipzig, Germany, March 28-30 1996.]

1 Introduction