Abstract
This paper exploits the point of view of constraint programming as computation in a logical system, namely constraint logic. We define the basic ingredients of constraint logic, such as constraint models and generalised polynomials. We show that constraint logic is an institution, and we internalise the study of constraint logic to the framework of category-based equational logic. By showing that constraint logic is a special case of category-based equational logic, we integrate the constraint logic programming paradigm into equational logic programming. Results include a Herbrand theorem for constraint logic programming characterising Herbrand models as initial models in constraint logic.
This research was partially supported by a grant for basic research in information science and technology from the Romanian Academy of Sciences.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Franz Baader and Klaus U. Schultz. On the Combination of Symbolic Constraints, Solution Domains, and Constraint Solvers. Technical Report 94-82, CIS-Universitat Muenchen, 1994.
L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation. Information and Computation, 121(2):172–192, 1995.
Garrett Birkhoff. On the structure of abstract algebras. Proceedings of the Cambridge Philosophical Society, 31:433–454, 1935.
H.-J. Bürckert. A Resolution Principle for a Logic with Restricted Quantifiers, volume 568 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1991.
Alain Colmerauer. An introduction to PrologIII. Technical report, Groupe Intelligence Artificielle, Faculte de Sciences de Luminy.
Virgil Căzănescu. Local equational logic. In Zoltan Esik, editor, Proceedings, 9th International Conference on Fundamentals of Computation Theory FCT'93, pages 162–170. Springer-Verlag, 1993. Lecture Notes in Computer Science, Volume 710.
Nachum Dershowitz. Computing with rewrite rules. Technical Report ATR-83(8478)-1, The Aerospace Corp., 1983.
Răzvan Diaconescu. The logic of Horn clauses is equational. Technical Report PRG-TR-3-93, Programming Research Group, University of Oxford, 1990.
Răzvan Diaconescu. Category-based Semantics for Equational and Constraint Logic Programming. PhD thesis, University of Oxford, 1994.
Răzvan Diaconescu. Completeness of category-based equational deduction. Mathematical Structures in Computer Science, 5(1):9–41, 1995.
Răzvan Diaconescu. Constraint institutions for combining solution and constraint domains, 1995. draft.
Răzvan Diaconescu. Category-based modularisation for equational logic programming. Acta Informatica, 33, 1996. To appear.
Răzvan Diaconescu. Completeness of semantic paramodulation: a category-based approach. Technical Report IS-RR-96-0006S, Japan Advanced Institute for Science and Technology, 1996.
Joseph Goguen. Theorem, Proving and Algebra. MIT, to appear 1996.
Joseph Goguen and Rod Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1):95–146, January 1992.
Joseph Goguen and Răzvan Diaconescu. An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science, 4(4):363–392, 1994.
Joseph Goguen and Răzvan Diaconescu. An introduction to category-based equational logic. In V.S. Alagar and Maurice Nivat, editors, Algebraic Methodology and Software Technology, volume 936 of Lecture Notes in Computer Science, pages 91–126. Springer, 1995.
Joseph Goguen and José Meseguer. Completeness of many-sorted equational logic. Houston Journal of Mathematics, 11(3):307–334, 1985.
Joseph Goguen and José Meseguer. Models and equality for logical programming. In Hartmut Ehrig, Giorgio Levi, Robert Kowalski, and Ugo Montanari, editors, Proceedings, 1987 TAPSOFT, pages 1–22. Springer, 1987. Lecture Notes in Computer Science, Volume 250.
Joxan Jaffar and Jean-Louis Lassez. Constraint logic programming. In 14th ACM Symposium on the Principles of Programming languages, pages 111–119. 1987.
Claude Kirchner, Hélène Kirchner, and M. Rusinowitch. Deduction with symbolic constraints. Revue d'Intelligence Artificielle, 4(3):9–52, 1990. Special issue on Automatic Deduction.
Claude Kirchner, Hélène Kirchner, and M. Vittek. Designing constraint logic programming languages using computational systems. In P. Van Hentenryck and V. Saraswat, editors, Principles and Practice of Constraint Programming. The Newport Papers., pages 131–158. 1995.
Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971.
José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, (93):73–155, 1992.
Peter Mosses. Unified algebras and institutions. In Proceedings, Fourth Annual Conference on Logic in Computer Science, pages 304–312. IEEE, 1989.
M. Stickel. Automated deduction by theory resolution. Journal of Automated Reasoning, 1(4):333–355, 1985.
Alfred Tarski. The semantic conception of truth. Philos. Phenomenological Research, 4:13–47, 1944.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Diaconescu, R. (1996). A category-based equational logic semantics to constraint programming. In: Haveraaen, M., Owe, O., Dahl, OJ. (eds) Recent Trends in Data Type Specification. ADT COMPASS 1995 1995. Lecture Notes in Computer Science, vol 1130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61629-2_44
Download citation
DOI: https://doi.org/10.1007/3-540-61629-2_44
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61629-0
Online ISBN: 978-3-540-70642-7
eBook Packages: Springer Book Archive