2012/10/05 by Iliano Cervesato, Cervesato, Iliano
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.1210.1653
To appear in Theory and Practice of Logic Programming
arxiv created 2012/10/05 · openalex publication_date 2012/10/05 · arxiv updated 2012/10/08 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.