Efficient resource management for linear logic proof search

DOI10.1016/S0304-3975(99)00173-5zbMath0958.03010MaRDI QIDQ1575929

Joshua S. Hodas, Frank Pfenning, Iliano Cervesato

Publication date: 23 August 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

theorem provinglinear logicresource managementlogic programmingproof search in type theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic programming (68N17) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items

Back to futures, A Survey of the Proof-Theoretic Foundations of Logic Programming, Towards substructural property-based testing, A linear logical framework, Unnamed Item, From cut-free calculi to automated deduction: the case of bounded contraction, Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic, Plans, actions and dialogues using linear logic, Efficient resource management for linear logic proof search, Resourceful program synthesis from graded linear types

Uses Software

• Elf
• Lolli

Cites Work

• Linear logic
• Forum: A multiple-conclusion specification logic
• Resolution calculus for the first order linear logic
• Logic programming in a fragment of intuitionistic linear logic
• Proof strategies in linear logic
• A linear logical framework
• Efficient resource management for linear logic proof search
• Uniform proofs as a foundation for logic programming
• Scoping constructs in logic programming: Implementation problems and their solution
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A Uniform Proof-theoretic Investigation of Linear Logic Programming
• Elf: A meta-language for deductive systems
• Resource-distribution via Boolean constraints
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item