Efficient resource management for linear logic proof search (Q1575929)

The essential difference between logic programming and theorem proving is the necessity to have the completely specified and understood operational semantics for a logic. Such semantics is realized, for example, in Prolog. But managing the clauses of a Prolog program is a simple task. For languages based on linear logic the task of managing the clauses of a program is more complicted. Linear logic views logical assumptions as consumable resources. Such a view raises a problem: How does the operational semantics deal with linear assumptions. This problem is called resource management problem. The authors show that for the logic based on intuitionistic implication, linear implication, additive conjunction, additive truth and universal quantification, each of the propositional connectives entails its own resource management problem and requires a new idea for its solution. They present a series of resource management systems designed to eliminate the nondeterminism in the distribution of linear formulas that undermines the efficiency of a direct implementation of this system. The paper studies the resource management problem for the language Lolli. These techniques form the foundation for the implementation of LLF, a type theory based on intuitionistic linear logic. Thus the work has been used directly for proof search in type theory.