Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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 Programming 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 http://www.informatik.uni-kiel.de/~curry/.
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. Maluszyʼnnski (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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leach, J., Nieva, S. (2001). A Higher-Order Logic Programming Language with Constraints. In: Kuchen, H., Ueda, K. (eds) Functional and Logic Programming. FLOPS 2001. Lecture Notes in Computer Science, vol 2024. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44716-4_7
Download citation
DOI: https://doi.org/10.1007/3-540-44716-4_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41739-2
Online ISBN: 978-3-540-44716-0
eBook Packages: Springer Book Archive