Efficient resource management for linear logic proof search
type: Item
instance of: scholarly article
title: Efficient resource management for linear logic proof search
zbMATH Open document ID: 0958.03010
DOI: 10.1016/S0304-3975(99)00173-5
author: Iliano Cervesato
author: Joshua S. Hodas
author: Frank Pfenning
published in: Theoretical Computer Science
publication date: 2000-08-23T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03F52
Mathematics Subject Classification ID: 68N17
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1495206
zbMATH Keywords: logic programming
zbMATH Keywords: theorem proving
zbMATH Keywords: linear logic
zbMATH Keywords: resource management
zbMATH Keywords: proof search in type theory
reviewed by: Nail Zamov
describes a project that uses: Elf
describes a project that uses: Lolli
MaRDI profile type: Publication
cites work: Q3357521
cites work: A linear logical framework
cites work: Q4501142
cites work: Linear logic
cites work: Resource-distribution via Boolean constraints
cites work: Logic programming in a fragment of intuitionistic linear logic
cites work: Q4222845
cites work: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
cites work: Forum: A multiple-conclusion specification logic
cites work: Uniform proofs as a foundation for logic programming
cites work: Resolution calculus for the first order linear logic
cites work: Scoping constructs in logic programming: Implementation problems and their solution
cites work: Q4472531
cites work: Elf: A meta-language for deductive systems
cites work: A Uniform Proof-theoretic Investigation of Linear Logic Programming
cites work: Proof strategies in linear logic
description: scientific article; zbMATH DE number 1495206