2026-08-20T15:39:26Zhttps://docta.ucm.es/rest/oai/request

oai:docta.ucm.es:20.500.14352/605882023-09-07T18:20:54Zcom_20.500.14352_14col_20.500.14352_21

Constraint logic programming with hereditary Harrop formulas Leach Albert, Javier Nieva Soto, Susana Rodríguez-Artalejo , Mario Maluszynski, Jan 004.43 Constraint systems Hereditary Harrop formulas Uniform proofs Goal solving Lenguajes de programación 1203.23 Lenguajes de Programación Conference: 1997 International Logic Programming Symposium (ILPS 97) Location: Port Washngton, New York Date: Oct 13-16, 1997 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 Spanish National Project Esprit BRA Working Group Sección Deptal. de Sistemas Informáticos y Computación Fac. de Ciencias Matemáticas TRUE pub 2023-06-20T21:03:50Z 2023-06-20T21:03:50Z 1997 book part https://hdl.handle.net/20.500.14352/60588 XXXX-XXXX TIC 95-0433-C03-01 CPD EP-22457 CCLII metadata only access MIT Press, Cambridge