An Improved Proof-Theoretic Compilation of Logic Programs

DOI10.1017/S1471068412000221zbMATH Open1260.68079arXiv1210.1653OpenAlexW1991813723MaRDI QIDQ4911140

Iliano Cervesato

Publication date: 13 March 2013

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

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.

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

zbMATH Keywords

compilationwell-moded logic programshereditary Harrop formulasabstract logic programming

Mathematics Subject Classification ID

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

Cites Work

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

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)