Hostname: page-component-cd9895bd7-gbm5v Total loading time: 0 Render date: 2024-12-25T04:37:56.034Z Has data issue: false hasContentIssue false
  • English
  • Français

Constraint Logic Programming with Hereditary Harrop formulas

Published online by Cambridge University Press:  25 June 2001

JAVIER LEACH ,
SUSANA NIEVA  and
MARIO RODRÍGUEZ-ARTALEJO
JAVIER LEACH
Affiliation:
Departamento Sistemas Informáticos y Programación, Av. Complutense s/n, Universidad Complutense de Madrid, E-28040 Madrid, Spain; e-mail: [email protected], [email protected], [email protected]
SUSANA NIEVA
Affiliation:
Departamento Sistemas Informáticos y Programación, Av. Complutense s/n, Universidad Complutense de Madrid, E-28040 Madrid, Spain; e-mail: [email protected], [email protected], [email protected]
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: [email protected], [email protected], [email protected]
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

constraint systemshereditary Harrop formulasuniform proofsgoal solving
Type
Research Article
Information
Theory and Practice of Logic Programming , Volume 1 , Issue 4 , July 2001 , pp. 409 - 445
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.)