Constraint Logic Programming with Hereditary Harrop Formula

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

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.
Appeared in Theory and Practice of Logic Programming, vol. 1, no. 4, 2001. Appeared in Theory and Practice of Logic Programming, vol. 1, no. 4, 2001

Keywords

Programming Languages, D.1.6; D.3.2

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/32090

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/cs/0404053
 http://arxiv.org/abs/cs/0404053

Collections

arXiv