Hostname: page-component-76fb5796d-x4r87 Total loading time: 0 Render date: 2024-04-26T10:26:44.128Z Has data issue: false hasContentIssue false

Constraint Logic Programming with Hereditary Harrop formulas

Published online by Cambridge University Press:  25 June 2001

JAVIER LEACH
Affiliation:
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
SUSANA NIEVA
Affiliation:
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
MARIO RODRÍGUEZ-ARTALEJO
Affiliation:
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.

Type
Research Article
Copyright
© 2001 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)