A higher-order logic programming language with constraints

Thumbnail Image
Full text at PDC
Publication Date
Advisors (or tutors)
Journal Title
Journal ISSN
Volume Title
Springer Verlag
Google Scholar
Research Projects
Organizational Units
Journal Issue
We present a framework for the combination of Constraint Logic Programming (tiCLP) and higher-order Hereditary Harrop Formulas (tihoHH). Our aim is to improve the expressiveness of traditional Logic Programming with the benefits of both fields: tiCLP and tihoHH. The result is denoted higher-order Hereditary Harrop Formulas with Constraints (hoHH(C)). The syntax of hoHH is introduced using lambda-terms and is enriched with a basic constraint system. Then an intuitionistic sequent calculus is defined for this combined logic, that preserves the property of an abstract logic programming language. In addition, a sound and complete procedure for goal solving is presented as a transformation system that explains the operational semantics.
The authors have been partially supported by the Spanish National Project TIC 98-0445-C03-02 TREND.
Clark, K.L., Negation as Failure, in: H. Gallaire and J. Minker (eds.), Logic and Databases 293-322, Plenum Press, 1978. Felty, A., Implementing Tactics and Tacticals in a Higher-Order Logic Program-ming Language, Journal of Automated Reasoning 11(1):43-81 (1993). Hanus, M. (ed.), Curry: an Integrated Functional Logic Language, Version 0.7, February 2, 2000. Available at Jaffar, J. and Maher, M.J., Constraint Logic Programming: A Survey, Journal of Logic Programming 19(20):503-581 (1994). Leach, J., Nieva, S. and Rodríguez-Artalejo, M., Constraint Logic Programming with Hereditary Harrop Formulas in: J. Ma luszynski (ed.), ILPS'97 307{321, MIT Press, 1997. Michaylov, S., Pfenning, F., Higher-Order Logic Programming as Constraint Logic Programming,in: Proc. of First Workshop on Principles and Practice of Constraint Programming, 221-229, Brown University, 1993. Miller, D., A Logical Analysis of Modules in Logic Programming, Journal of Logic Programming 6(1,2):79-108 (1989). Miller, D., Nadathur, G., Pfenning, F. and Scedrov, A., Uniform Proofs as a Foundation for Logic Programming, Annals of Pure and Applied Logic 51:125-157 (1991). Miller, D., Nadathur, G. and Scedrov, A., Hereditary Harrop Formulas and Uniform Proof Systems, in: D. Gries (ed.), LICS'87 98-105, IEEE Comp. Soc. Press, 1987. Nadathur, G. and Miller, D., An Overview of Prolog, in: K.A. Bowen and R. A. Kowalski (eds.), ICLP'88 810-827, MIT Press, 1988. Nerode, A., Some Lectures on Intuitionistic Logic, in: S. Homer, A. Nerode, R.A. Platek, G.E. Sacks, A. Scedrov (eds.), LCS'88 12-59, Springer LNM 1429, 1988. Saraswat, V., The Category of Constraint Systems is Cartesian Closed, in: LICS'92 341-345, IEEE Comp. Soc. Press, 1992. Tarski, A., A Decision Method for Elementary Algebra and Geometry , University of California Press, 1951.