An improved proof-theoretic compilation of logic programs

DOI10.1017/S1471068412000221MaRDI QIDQ4911140zbMATH OpenOpenAlexFDO

Authors Iliano Cervesato

Publication date 13 March 2013

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1210.1653

zbMATH Keywords

abstract logic programmingcompilationhereditary Harrop formulaswell-moded logic programs

Mathematics Subject Classification ID

Logic programming (68N17) Theory of compilers and interpreters (68N20)

Abstract: In prior work, we showed that logic programming compilation can be given a proof-theoretic justification for generic abstract logic programming languages, and demonstrated this technique in the case of hereditary Harrop formulas and their linear variant. Compiled clauses were themselves logic formulas except for the presence of a second-order abstraction over the atomic goals matching their head. In this paper, we revisit our previous results into a more detailed and fully logical justification that does away with this spurious abstraction. We then refine the resulting technique to support well-moded programs efficiently.

Recommendations

• scientific article; zbMATH DE number 1420805
• A proof procedure for the logic of hereditary Harrop formulas
• Proofs as computations in linear logic
• A practical framework for theabstract interpretation of logic programs
• Declarative compilation for constraint logic programming

Cites work

• A linear logical framework
• A verified prolog compiler for the Warren Abstract Machine
• Automatic mode inference for logic programs
• Decidability of higher-order matching
• Logic programming in a fragment of intuitionistic linear logic
• Uniform proofs as a foundation for logic programming

Cited in

(10)

• Some results and experiments in programming techniques for propositional logic
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Declarative compilation for constraint logic programming
• scientific article; zbMATH DE number 4033137 (Why is no real title available?)
• A verified prolog compiler for the Warren Abstract Machine
• scientific article; zbMATH DE number 512886 (Why is no real title available?)
• scientific article; zbMATH DE number 1543038 (Why is no real title available?)
• scientific article; zbMATH DE number 2087569 (Why is no real title available?)
• scientific article; zbMATH DE number 1420805 (Why is no real title available?)
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic

Describes a project that uses

Uses Software

• Twelf

This page was built for publication: An improved proof-theoretic compilation of logic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4911140)