2026-08-20T06:01:28Zhttps://docta.ucm.es/rest/oai/requestoai:docta.ucm.es:20.500.14352/605882023-09-07T18:20:54Zcom_20.500.14352_14col_20.500.14352_21
Docta Complutense
author
Leach Albert, Javier
author
Nieva Soto, Susana
author
RodrÃguez-Artalejo , Mario
editor
Maluszynski, Jan
2023-06-20T21:03:50Z
2023-06-20T21:03:50Z
1997
0-262-63180-6
https://hdl.handle.net/20.500.14352/60588
http://dl.acm.org/citation.http://dl.acm.org/citation.cfm?id=271419&CFID=149252991&CFTOKEN=67712323
http://dl.acm.org/dl.cfm?CFID=149252991&CFTOKEN=67712323
Constraint logic programing (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 building disjunctions of computed answers, as well as a more declarative formulation of a known completeness theorem for HH
Constraint logic programming with hereditary Harrop formulas
book part