Constraint Logic Programming with Hereditary Harrop formulas
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.
Key Words: constraint systems; hereditary Harrop formulas; uniform proofs; goal solving.
1 This is a substantially revised and extended version of an earlier paper (Leach, Nieva and Rodríguez-Artalejo, 1997). The authors have been partially supported by the Spanish National Project TIC 98-0445-C03-02 TREND and the Esprit BRA Working Group EP-22457 CCLII.