Constraint Logic Programming with Hereditary Harrop formulas
| dc.contributor.author | Leach Albert, Javier | |
| dc.contributor.author | Nieva Soto, Susana | |
| dc.contributor.author | Rodríguez-Artalejo, Mario | |
| dc.date.accessioned | 2023-06-20T17:04:12Z | |
| dc.date.available | 2023-06-20T17:04:12Z | |
| dc.date.issued | 2001-07 | |
| dc.description | This is a substantially revised and extended version of an earlier paper (Leach, Nieva and Rodrguez-Artalejo, 1997). The authors have been partially supported by the Spanish National Project TIC 98-0445-C03-02 TREND and the Esprit BRA Working Group EP-22457 CCLII. | |
| dc.description.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. | |
| dc.description.department | Sección Deptal. de Sistemas Informáticos y Computación | |
| dc.description.faculty | Fac. de Ciencias Matemáticas | |
| dc.description.refereed | TRUE | |
| dc.description.sponsorship | TIC | |
| dc.description.sponsorship | TREND | |
| dc.description.sponsorship | Esprit BRA Working Group | |
| dc.description.status | pub | |
| dc.eprint.id | https://eprints.ucm.es/id/eprint/17171 | |
| dc.identifier.doi | 10.1017/S1471068401001041 | |
| dc.identifier.issn | 1471-0684 | |
| dc.identifier.officialurl | http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=78817 | |
| dc.identifier.relatedurl | http://journals.cambridge.org/action/login | |
| dc.identifier.uri | https://hdl.handle.net/20.500.14352/57721 | |
| dc.issue.number | 4 | |
| dc.journal.title | Theory and Practice of Logic Programming | |
| dc.language.iso | eng | |
| dc.page.final | 445 | |
| dc.page.initial | 409 | |
| dc.publisher | Cambridge Univ Press | |
| dc.relation.projectID | 98-0445-C03-02 | |
| dc.relation.projectID | EP-22457 CCLII | |
| dc.rights.accessRights | restricted access | |
| dc.subject.cdu | 004.43 | |
| dc.subject.keyword | Constraint systems | |
| dc.subject.keyword | Hereditary Harrop formulas | |
| dc.subject.keyword | Uniform proofs | |
| dc.subject.keyword | Goal solving | |
| dc.subject.ucm | Lenguajes de programación | |
| dc.subject.unesco | 1203.23 Lenguajes de Programación | |
| dc.title | Constraint Logic Programming with Hereditary Harrop formulas | |
| dc.type | journal article | |
| dc.volume.number | 1 | |
| dcterms.references | Andreka, H. and Nemeti, I. (1978) The generalized completeness of Horn Predicate Logic as a programming language. Acta Cybernetica, 4, 3-10. Clark, K. L. (1978) Negation as failure. In: Gallaire, H. and Minker, J. (eds.), Logic and Databases, pp. 293-322. Plenum Press, New York. CLP with Hereditary Harrop formulas 445 Comon, H., Haberstrau, M. and Jouannaud, J. P. (1994) Cycle-syntacticness, and shallow theories. Information & Computation, 111, 154-191. Cohen, J. (1990) Constraint Logic Programming languages. Comm. ACM, 35(7), 52-68. Comon, H. (1993) Complete axiomatizations of some quotient term algebras. Theor. Comput. Sci. 118, 167-191. Darlington, J. and Guo, Y. (1994) Constraint Logic Programming in the Sequent Calculus. In: Pfenning, F. (ed.), LPAR'94. LNAI 822, pp. 200-213. Springer-Verlag. Dershowitz, N. and Manna, Z. (1979) Proving termination with multiset ordering. Comm. ACM, 22(8), 465-476. Hodas, J. S. (1994) Logic Programming in Intuitionistic Linear Logic: Theory, Design and Implementation. PhD Thesis, University of Pennsylvania. Jaar, J. and Lassez, J. L. (1987) Constraint Logic Programming. Proc. 14th ACM Symposium on Principles of Programming Languages, pp. 111-119. Jaar, J. and Michaylov, S. (1987) Methodology and implementation of CLP systems. In: Lassez, J. L. (ed.), ICLP'87, pp. 196-218. MIT Press. Jaar, J. and Maher, M. J. (1994) Constraint Logic Programming: A survey. J. Logic Programming,19(20), 503-581. Jaar,J.,Maher,M.J.,Marriott,K.and Stuckey,P.(1996)The Semantics of Constraint Logic Programs. Technical Report TR 96/39,Department of Computer Science,University of Melbourne Jaar, J., Michaylov, S., Stuckey, P. and Yap, R. (1992) The CLP(R) Language and System. ACM Trans. Programming Lang., 14(3), 339-395. Leach, J., Nieva, S. and Rodrguez-Artalejo, M. (1997) Constraint Logic Programming with Hereditary Harrop formulas. In: Ma luszyn ski, J. (ed.), ILPS'97, pp. 307-321. MIT Press. Maher, M. (1987) Logic semantics for a class of committed-choice programs. In: Lassez, J. L. (editor), ICLP'87, pp. 858-876. MIT Press. Miller, D. (1989) A logical analysis of modules in logic programming. J. Logic Programming, 6(1, 2), 79-108. Miller, D. (1992) Unication under a mixed prex. J. Symbolic Computation, 14, 321-358. Miller, D. and Nadathur, G. (1986) Higher-order logic programming. In: Shapiro, E. (ed.), ICLP'86: LNCS 225, pp. 448-462. Springer-Verlag. Miller, D., Nadathur, G., Pfenning, F. and Scedrov, A. (1991) Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic, 51(1-2), 125-157. Miller, D., Nadathur, G. and Scedrov, A. (1987) Hereditary Harrop formulas and uniform proof systems. In: Gries, D. (ed.), LICS'87, pp. 98-105. IEEE Press. Nadathur, G. (1993) A proof procedure for the logic of Hereditary Harrop formulas. J. Automated Reasoning, 11, 115-145. Nadathur, G. and Miller, D. (1988) An overview of -Prolog. In: Bowen, K. A. and Kowalski, R. A. (eds.), ICLP'88, pp. 810-827. MIT Press. Saraswat, V. (1992) The category of constraint systems is Cartesian closed. LICS'92, pp. 341-345. IEEE Press. Smolka, G. and Treinen, R. (1994) Records for logic programming. J. Logic Programming, 18(3), 229-258. Van Emden, M. H. and Kowalski, R. H. (1976) The semantics of predicate logic as a programming language. J. ACM, 23(4), 733-742. Tarski, A. (1951) A Decision Method for Elementary Algebra and Geometry. University of California Press. | |
| dspace.entity.type | Publication | |
| relation.isAuthorOfPublication | 700e0e32-6c94-43f9-9c48-4c42ef20957b | |
| relation.isAuthorOfPublication | 21132b4a-0809-4135-9a71-0b771813a8e9 | |
| relation.isAuthorOfPublication.latestForDiscovery | 700e0e32-6c94-43f9-9c48-4c42ef20957b |
Download
Original bundle
1 - 1 of 1