Constraint logic programming with hereditary Harrop formulas

dc.book.titleLogic programming. Proceedings of the international symposium (ILPS’97)
dc.contributor.authorLeach Albert, Javier
dc.contributor.authorNieva Soto, Susana
dc.contributor.authorRodríguez-Artalejo , Mario
dc.contributor.editorMaluszynski, Jan
dc.date.accessioned2023-06-20T21:03:50Z
dc.date.available2023-06-20T21:03:50Z
dc.date.issued1997
dc.descriptionConference: 1997 International Logic Programming Symposium (ILPS 97) Location: Port Washngton, New York Date: Oct 13-16, 1997
dc.description.abstractConstraint 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
dc.description.departmentSección Deptal. de Sistemas Informáticos y Computación
dc.description.facultyFac. de Ciencias Matemáticas
dc.description.refereedTRUE
dc.description.sponsorshipSpanish National Project
dc.description.sponsorshipEsprit BRA Working Group
dc.description.statuspub
dc.eprint.idhttps://eprints.ucm.es/id/eprint/17267
dc.identifier.isbn0-262-63180-6
dc.identifier.officialurlhttp://dl.acm.org/citation.http://dl.acm.org/citation.cfm?id=271419&CFID=149252991&CFTOKEN=67712323
dc.identifier.relatedurlhttp://dl.acm.org/dl.cfm?CFID=149252991&CFTOKEN=67712323
dc.identifier.urihttps://hdl.handle.net/20.500.14352/60588
dc.page.final321
dc.page.initial307
dc.page.total423
dc.publication.placePort Washington, New York
dc.publisherMIT Press, Cambridge
dc.relation.projectIDTIC 95-0433-C03-01 CPD
dc.relation.projectIDEP-22457 CCLII
dc.rights.accessRightsmetadata only access
dc.subject.cdu004.43
dc.subject.keywordConstraint systems
dc.subject.keywordHereditary Harrop formulas
dc.subject.keywordUniform proofs
dc.subject.keywordGoal solving
dc.subject.ucmLenguajes de programación
dc.subject.unesco1203.23 Lenguajes de Programación
dc.titleConstraint logic programming with hereditary Harrop formulas
dc.typebook part
dcterms.referencesAndreka, 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. 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.typePublication
relation.isAuthorOfPublication700e0e32-6c94-43f9-9c48-4c42ef20957b
relation.isAuthorOfPublication21132b4a-0809-4135-9a71-0b771813a8e9
relation.isAuthorOfPublication.latestForDiscovery700e0e32-6c94-43f9-9c48-4c42ef20957b

Download