A category-based equational logic semantics to constraint programming

  • Răzvan Diaconescu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1130)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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.Google Scholar
  2. 2.
    L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation. Information and Computation, 121(2):172–192, 1995.Google Scholar
  3. 3.
    Garrett Birkhoff. On the structure of abstract algebras. Proceedings of the Cambridge Philosophical Society, 31:433–454, 1935.Google Scholar
  4. 4.
    H.-J. Bürckert. A Resolution Principle for a Logic with Restricted Quantifiers, volume 568 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1991.Google Scholar
  5. 5.
    Alain Colmerauer. An introduction to PrologIII. Technical report, Groupe Intelligence Artificielle, Faculte de Sciences de Luminy.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    Nachum Dershowitz. Computing with rewrite rules. Technical Report ATR-83(8478)-1, The Aerospace Corp., 1983.Google Scholar
  8. 8.
    Răzvan Diaconescu. The logic of Horn clauses is equational. Technical Report PRG-TR-3-93, Programming Research Group, University of Oxford, 1990.Google Scholar
  9. 9.
    Răzvan Diaconescu. Category-based Semantics for Equational and Constraint Logic Programming. PhD thesis, University of Oxford, 1994.Google Scholar
  10. 10.
    Răzvan Diaconescu. Completeness of category-based equational deduction. Mathematical Structures in Computer Science, 5(1):9–41, 1995.Google Scholar
  11. 11.
    Răzvan Diaconescu. Constraint institutions for combining solution and constraint domains, 1995. draft.Google Scholar
  12. 12.
    Răzvan Diaconescu. Category-based modularisation for equational logic programming. Acta Informatica, 33, 1996. To appear.Google Scholar
  13. 13.
    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.Google Scholar
  14. 14.
    Joseph Goguen. Theorem, Proving and Algebra. MIT, to appear 1996.Google Scholar
  15. 15.
    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.Google Scholar
  16. 16.
    Joseph Goguen and Răzvan Diaconescu. An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science, 4(4):363–392, 1994.Google Scholar
  17. 17.
    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.Google Scholar
  18. 18.
    Joseph Goguen and José Meseguer. Completeness of many-sorted equational logic. Houston Journal of Mathematics, 11(3):307–334, 1985.Google Scholar
  19. 19.
    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.Google Scholar
  20. 20.
    Joxan Jaffar and Jean-Louis Lassez. Constraint logic programming. In 14th ACM Symposium on the Principles of Programming languages, pages 111–119. 1987.Google Scholar
  21. 21.
    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.Google Scholar
  22. 22.
    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.Google Scholar
  23. 23.
    Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971.Google Scholar
  24. 24.
    José Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, (93):73–155, 1992.Google Scholar
  25. 25.
    Peter Mosses. Unified algebras and institutions. In Proceedings, Fourth Annual Conference on Logic in Computer Science, pages 304–312. IEEE, 1989.Google Scholar
  26. 26.
    M. Stickel. Automated deduction by theory resolution. Journal of Automated Reasoning, 1(4):333–355, 1985.Google Scholar
  27. 27.
    Alfred Tarski. The semantic conception of truth. Philos. Phenomenological Research, 4:13–47, 1944.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Răzvan Diaconescu
    • 1
  1. 1.Institute of Mathematics of the Romanian AcademyRomania

Personalised recommendations