Theory and Practice of Logic Programming

Table of Contents - 2001 - Volume 1, Issue 04  


Constraint Logic Programming with Hereditary Harrop formulas

JAVIER LEACH a1, SUSANA NIEVA a1 and MARIO RODRÍGUEZ-ARTALEJO a1 1
a1 Departamento Sistemas Informáticos y Programación, Av. Complutense s/n, Universidad Complutense de Madrid, E-28040 Madrid, Spain; e-mail: leach@sip.ucm.es, nieva@sip.ucm.es, mario@sip.ucm.es

Abstract

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.

Footnotes

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.