Constraint Logic Programming with Hereditary Harrop Formula
<|reference_start|>Constraint Logic Programming with Hereditary Harrop Formula: Constraint Logic Programming (CLP) and Hereditary Harrop formulas (HH) are two well known ways to enhance the expressivity of Horn clauses. In this paper, we present a novel combination of these two approaches. We show how to enrich the syntax and proof theory of HH with the help of a given constraint system, in such a way that the key property of HH as a logic programming language (namely, the existence of uniform proofs) is preserved. We also present a procedure for goal solving, showing its soundness and completeness for computing answer constraints. As a consequence of this result, we obtain a new strong completeness theorem for CLP that avoids the need to build disjunctions of computed answers, as well as a more abstract formulation of a known completeness theorem for HH.<|reference_end|>
@article{leach2004constraint,
    title={Constraint Logic Programming with Hereditary Harrop Formula},
    author={Javier Leach, Susana Nieva, Mario Rodriguez-Artalejo},
    journal={arXiv preprint arXiv:cs/0404053},
    year={2004},
    archivePrefix={arXiv},
    eprint={cs/0404053},
    primaryClass={cs.PL}
}