Abstract
Implementations of Constraint Logic Programming (CLP) systems are often incomplete with respect to the theories they are intended to implement. This paper studies two issues that arise in dealing with these incomplete implementations. First, the notion of incomplete “satisfiability function” (the analogue of unification) is formally defined, and the question of which such functions are reasonable is studied. Second, techniques are given for formally (proof-theoretically) specifying an intended CLP theory or a characterizing an existing CLP system, for the purpose of proving soundness and completeness results. Notions from linear logic and the notion of Henkinness of the theory are shown to be important here.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
James H. Andrews. Proof-theoretic characterisations of logic programming. In Mathematical Foundations of Computer Science, volume 379 of Lecture Notes in Computer Science, pages 145–154, Porabka-Kozubnik, Poland, 1989. Springer.
Alain Colmerauer. Prolog and infinite trees. In K. L. Clark and S.-A. Tärnlund, editors, Logic Programming, pages 231–251. Academic Press, 1983.
Thom Frühwirth. Constraint simplification rules. Technical Report 92-18, ECRC, Munich, Germany, July 1992.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
Masami Hagiya and Takafumi Sakurai. Foundation of logic programming based on inductive definition. New Generation Computing, 2:59–77, 1984.
Markus Höhfeld and Gert Smolka. Definite relations over constraint languages. Technical Report 53, LILOG, IBM Deutschland, Stuttgart, Germany, October 1988. To appear in Journal of Logic Programming.
Lars Hallnäs and Peter Schroeder-Heister. A proof-theoretic approach to logic programming I: Clauses as rules. Journal of Logic and Computation, 1(2), 1990.
Joxan Jaffar and Jean-Louis Lassez. Constraint logic programming. In Proceedings of the Conference on Principles of Programming Languages, Munich, 1987.
Joxan Jaffar, Spiro Michaylov, Peter J. Stuckey, and Roland H. C. Yap. The CLP(R) language and system. ACM Transactions on Programming Languages and Systems, 14(3):339–395, July 1992.
Stephen Cole Kleene. Introduction to Metamathematics, volume 1 of Bibliotheca Mathematica. North-Holland, Amsterdam, 1952.
Alan Mackworth. Constraint satisfaction. Technical Report 85-15, Department of Computer Science, University of British Columbia, September 1985.
Michael J. Maher. Complete axiomatizations of the algebras of finite, rational and infinite trees. In Proceedings of the Third Annual Symposium on Logic In Computer Science, pages 348–357, Edinburgh, July 1988. Computer Society Press.
Michael J. Maher. A logic programming view of CLP. In Proceedings of the Tenth International Conference on Logic Programming, pages 737–753, Budapest, July 1993. MIT Press.
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.
James Donald Monk. Mathematical Logic, volume 37 of Graduate texts in mathematics. Springer-Verlag, New York, 1976.
Dana Scott. Domains for denotational semantics. In International Colloquium on Automata, Languages, and Programming, 1982.
Joseph Shoenfield. Mathematical Logic. Addison-Wesley, Reading, Mass., 1967.
Maarten H. van Emden and John W. Lloyd. A logical reconstruction of Prolog II. Journal of Logic Programming, 2:143–149, 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andrews, J.H. (1994). Foundational issues in implementing constraint logic programming systems. In: Sannella, D. (eds) Programming Languages and Systems — ESOP '94. ESOP 1994. Lecture Notes in Computer Science, vol 788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57880-3_5
Download citation
DOI: https://doi.org/10.1007/3-540-57880-3_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57880-2
Online ISBN: 978-3-540-48376-2
eBook Packages: Springer Book Archive