System description: An equational constraints solver

  • Nicolas Peltier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)


Symbolic Computation Conjunctive Normal Form Universal Quantifier Automate Deduction Equational Formula 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    C. Bourely, R. Caferra, and N. Peltier. A method for building models automatically. Experiments with an extension of Otter. In Proceedings of CADE-12, pages 72–86. Springer, 1994. LNAI 814.Google Scholar
  2. 2.
    R. Caferra and M. Herment. A generic graphic framework for combining inference tools and editing proofs and formulae. Journal of Symbolic Computation, 19(2):217–243, 1995.CrossRefzbMATHGoogle Scholar
  3. 3.
    R. Caferra and N. Peltier. Decision procedures using model building techniques. In Proceeding of Computer Science Logic, CSL '95, pages 130–144. Springer, LNCS 1092, 1996.Google Scholar
  4. 4.
    R. Caferra and N. Zabel. A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation, 13:613–641, 1992.MathSciNetzbMATHCrossRefGoogle Scholar
  5. 5.
    A. Colmerauer. Equations and inequations on finite or infinite trees. In FGCS'84, pages 85–99, November 1984.Google Scholar
  6. 6.
    H. Comon. Inductive proofs by specification transformation. In Proc. of RTA 89. Springer, 1989.Google Scholar
  7. 7.
    H. Comon. Disunification: a survey. In Jean-Louis Lassez, Gordon Plotkin, editors. Computational logic: Essays in Honor of Alan Robinson. MIT Press, 1991.Google Scholar
  8. 8.
    H. Comon and C. Delor. Equational formulae with membership constraints. Information and Computation, 112(2):167–216, August 1994.CrossRefMathSciNetzbMATHGoogle Scholar
  9. 9.
    H. Comon and P. Lescanne. Equational problems and disunification. Journal of Symbolic Computation, 7:371–475, 1989.MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    C. Delor. Transformation de problèmes équationels. Internal report, Ecole Normale Supérieure, Paris (in French), 1989.Google Scholar
  11. 11.
    S. Klingenbeck. Counter Examples in Semantic Tableaux. PhD thesis, University of Karlsruhe, 1996.Google Scholar
  12. 12.
    K. Kunen. Answer sets and negation as failure. In J. L. Lassez, editor, Proceeding of the Fourth International Conference on Logic Programming, pages 219–227. The MIT Press, May 1987.Google Scholar
  13. 13.
    D. Lugiez. A deduction procedure for first order programs. In F. Levi and M. Martelli, editors, Proceedings of the sixth International Conference on Logic Programming pages 585–599. The MIT Press, July 1989.Google Scholar
  14. 14.
    M. 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 248–357. IEEE Computer Society, 1988.Google Scholar
  15. 15.
    A. Mal'cev. The Metamathematics of Algebraic Systems: Collected Papers 1936–1967, chapter Axiomatizable classes of locally free algebra of various type, pages 262–281. Benjamin Franklin Wells editor, North Holland, 1971. chapter 23.Google Scholar
  16. 16.
    W. W. McCune. OTTER 3.0 Reference Manual and Guide. Argonne National Laboratory, 1994.Google Scholar
  17. 17.
    M. Mehl. Gleichungsdefinierte probleme. lösungsmethoden und anwendungen bei algebraischen Spezifikationen. Projekarbeit, UniversitÄt Kaiserlautern (in German), 1988.Google Scholar
  18. 18.
    N. Peltier. Increasing the capabilities of model building by constraint solving with terms with integer exponents. Journal of Symbolic Computation, 24:59–101, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    N. Peltier. Nouvelles Techniques pour la Construction de Modèles finis ou infinis en Déduction Automatique. PhD thesis, Institut National Polytechnique de Grenoble, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Nicolas Peltier
    • 1
  1. 1.Laboratory LEIBNIZ-IMAGGrenoble CedexFrance

Personalised recommendations