Skip to main content
SpringerLink
Log in

On the use of constraints in automated deduction

  • Conference paper
  • First Online:
Constraint Programming: Basics and Trends (TCS School 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 910))

Included in the following conference series:

Abstract

This paper presents three approaches dealing with constraints in automated deduction. Each of them illustrates a different point. The expression of strategies using constraints is shown through the example of a completion process using ordered and basic strategies. The schematization of complex unification problems through constraints is illustrated by the example of an equational theorem prover with associativity and commutativity axioms. The incorporation of built-in theories in a deduction process is done for a narrowing process which solves queries in theories defined by rewrite rules with built-in constraints. Advantages of using constraints in automated deduction are emphasized and new challenging problems in this area are pointed out.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Franz Baader and Klaus Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N.Y., USA), pages 50–65, 1992.

    Google Scholar 

  2. L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. Theoretical Computer Science, 67(2–3):173–202, October 1989.

    Google Scholar 

  3. L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):1–31, 1994.

    Google Scholar 

  4. L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N.Y., USA), pages 462–476, 1992.

    Google Scholar 

  5. L. Bachmair and D. A. Plaisted. Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation, 1:329–349, 1985.

    Google Scholar 

  6. T. B. Baird, G. E. Peterson, and Ralph W. Wilkerson. Complete sets of reductions modulo associativity, commutativity and identity. In N. Dershowitz, editor, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA), volume 355 of Lecture Notes in Computer Science, pages 29–44. Springer-Verlag, April 1989.

    Google Scholar 

  7. 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 

  8. Jacques Chabin. Unification Générale par Surréduction Ordonnée Contrainte et Surréduction Dirigée. Thèse de Doctorat d'Université, Université d'Orléans, January 1994.

    Google Scholar 

  9. H. Comon. Completion of rewrite systems with membership constraints. In W. Kuich, editor, Proceedings of ICALP 92, volume 623 of Lecture Notes in Computer Science. Springer-Verlag, 1992.

    Google Scholar 

  10. N. Dershowitz and J.-P. Jouannaud. Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pages 244–320. Elsevier Science Publishers B. V. (North-Holland), 1990. Also as: Research report 478, LRI.

    Google Scholar 

  11. N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, pages 244–320. Elsevier Science Publishers B. V. (North-Holland), 1990.

    Google Scholar 

  12. E. Domenjoud. Outils pour la déduction automatique dans les théories associatives-commutatives. Thèse de Doctorat d'Université, Université de Nancy 1, September 1991.

    Google Scholar 

  13. E. Domenjoud. A technical note on AC-unification. the number of minimal unifiers of the equation αx 1+...+αx p ≐ AC βy 1+...βy q . Journal of Automated Reasoning, 8:39–44, 1992. Also as research report CRIN 89-R-2.

    Google Scholar 

  14. M. Fernández. Narrowing based procedures for equational disunification. Applicable Algebra in Engineering, Communication and Computation, 3:1–26, 1992.

    Google Scholar 

  15. A. Frisch and Scherl R. A general framework for modal deduction. In J. A. Allen, R. Fikes, and E. Sandewall, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Second International Conference, San Mateo, CA, USA, 1991.

    Google Scholar 

  16. G. Huet. Constrained Resolution: A Complete Method for Higher Order Logic. PhD thesis, Case Western Reserve University, 1972.

    Google Scholar 

  17. J.-P. Jouannaud and Héléne Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing, 15(4):1155–1194, 1986. Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City (USA), 1984.

    Google Scholar 

  18. J.-P. Jouannaud and C. Marché. Completion modulo associativity, commutativity and identity (AC1). In A. Miola, editor, Proceedings of DISCO'90, volume 429 of Lecture Notes in Computer Science, pages 111–120. Springer-Verlag, April 1990.

    Google Scholar 

  19. Claude Kirchner and Héléne Kirchner. Constrained equational reasoning. In Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, Portland (Oregon), pages 382–389. ACM Press, July 1989. Report CRIN 89-R-220.

    Google Scholar 

  20. 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 

  21. H. Kirchner and P.-E. Moreau. Prototyping completion with constraints using computational systems. Technical report submitted, 1994.

    Google Scholar 

  22. H. Kirchner and C. Ringeissen. Constraint solving by narrowing in combined algebraic domains. In P. Van Hentenryck, editor, Proc. 11th International Conference on Logic Programming, pages 617–631. The MIT press, 1994.

    Google Scholar 

  23. C. Lynch and W. Snyder. Redundancy criteria for constrained completion. In C. Kirchner, editor, Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada), volume 690 of Lecture Notes in Computer Science, pages 2–16. Springer-Verlag, 1993.

    Google Scholar 

  24. U. Martin and T. Nipkow. Ordered rewriting and confluence. In M. E. Stickel, editor, Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture Notes in Computer Science, pages 366–380. Springer-Verlag, 1990.

    Google Scholar 

  25. P. Narendran and M. Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In R. V. Book, editor, Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy). Springer-Verlag, 1991.

    Google Scholar 

  26. R. Nieuwenhuis and A. Rubio. Basic superposition is complete. In B. Krieg-Brückner, editor, Proceedings of ESOP'92, volume 582 of Lecture Notes in Computer Science, pages 371–389. Springer-Verlag, 1992.

    Google Scholar 

  27. R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In D. Kapur, editor, Proceedings of CADE-11, volume 607 of Lecture Notes in Computer Science, pages 477–491. Springer-Verlag, 1992.

    Google Scholar 

  28. R. Nieuwenhuis and A. Rubio. AC-superposition with constraints: no AC-unifiers needed. In A. Bundy, editor, Proceedings 12th International Conference on Automated Deduction, Nancy (France), volume 814 of Lecture Notes in Artificial Intelligence, pages 545–559. Springer-Verlag, June 1994.

    Google Scholar 

  29. G. E. Peterson. Complete sets of reductions with constraints. In M. E. Stickel, editor, Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture Notes in Computer Science, pages 381–395. Springer-Verlag, 1990.

    Google Scholar 

  30. A. Rubio and R. Nieuwenhuis. A precedence-based total AC-compatible ordering. In C. Kirchner, editor, Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada), volume 690 of Lecture Notes in Computer Science, pages 374–388. Springer-Verlag, 1993.

    Google Scholar 

  31. G. Smolka. Logic Programming over Polymorphically Order-Sorted Types. PhD thesis, FB Informatik, Universität Kaiserslautern, Germany, 1989.

    Google Scholar 

  32. M. Stickel. Automated deduction by theory resolution. Journal of Automated Reasoning, 1(4):285–289, 1985.

    Google Scholar 

  33. L. Vigneron. Associative-Commutative Deduction with Constraints. In A. Bundy, editor, Proceedings 12th International Conference on Automated Deduction, Nancy (France), volume 814 of Lecture Notes in Artificial Intelligence, pages 530–544. Springer-Verlag, June 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIN-CNRS & INRIA-Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy Cedex

    Hélène Kirchner

Authors
  1. Hélène Kirchner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andreas Podelski

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kirchner, H. (1995). On the use of constraints in automated deduction. In: Podelski, A. (eds) Constraint Programming: Basics and Trends. TCS School 1994. Lecture Notes in Computer Science, vol 910. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59155-9_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-59155-9_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59155-9

  • Online ISBN: 978-3-540-49200-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation