Skip to main content
SpringerLink
Log in

Complete sets of reductions with constraints

  • Conference paper
  • First Online:
Book cover 10th International Conference on Automated Deduction (CADE 1990)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 449))

Included in the following conference series:

Abstract

We show that by constraining the substitutions allowed in some of the rules, it is possible to find complete sets of reductions for equational theories which include non-orientable equations such as commutativity without requiring a special unification algorithm. We develop the theory for such constrained reductions and we exhibit complete sets for semilattices, boolean algebras, and ternary boolean algebras.

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. L. Bachmair, N. Dershowitz, and D. Plaisted, “Completion Without Failure,” Preliminary Proceedings of the Colloquium on the Resolution of Equations in Algebraic Structures, Lakeway Texas, May 4–6, 1987, sponsored by Microelectronics and Computer Technology Corporation, M. Nivat and H Aït-Kaci, organizers.

    Google Scholar 

  2. T. Baird, G. Peterson, and R. Wilkerson, “Complete Sets of Reductions Modulo Associativity, Commutativity and Identity,” Lecture Notes in Computer Science 355 Rewriting Techniques and Applications, RAT-89, N. Dershowitz, ed., Springer-Verlag, 1989, 29–44.

    Google Scholar 

  3. C. Chang and R. Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973.

    Google Scholar 

  4. H. Comon, “Solving Inequations in Term Algebras,” Fifth Symp. on Logic in Computer Science, LICS 90, 1990.

    Google Scholar 

  5. N. Dershowitz, “Termination of rewriting,” J. Symbolic Computation, 3 (1987), 69–116.

    Google Scholar 

  6. N. Dershowitz, M. Okaba, and G. Sivakumar, “Canonical Conditional Rewrite Systems,” Lecture Notes in Computer Science 310, 9th International Conference on Automated Deduction E. Lusk and R. Overbeek editors, 1988, 538–549.

    Google Scholar 

  7. R. Göbel, “Completion of Globally Finite Term Rewriting Systems for Inductive Proofs,” Universität Kaiserslautern SEKI-REPORT SR-86-06, June 1986.

    Google Scholar 

  8. R. Göbel, “Ground Confluence,” Lecture Notes in Computer Science 256 Rewriting Techniques and Applications, RTA-87, P. Lescanne, ed., Springer-Verlag, 1987, 156–167.

    Google Scholar 

  9. A. A. Grau, “Ternary boolean algebra,” Bulletin of the American Mathematical Society, 53 (1947), 567–572.

    Google Scholar 

  10. J.-P. Jouannaud and H. Kirchner, “Completion of a set of rules modulo a set of equations,” SIAM Journal of Computing, 15 (1986), 1155–1194.

    Google Scholar 

  11. D. Knuth and P. Bendix, “Simple word problems in universal algebras,” Computational Problems in Abstract Algebras, J. Leech, ed., Pergamon Press, Oxford, England, 1970, 263–297.

    Google Scholar 

  12. D. Kapur, P. Narendran, and F. Otto, “On Ground-Confluence of Term Rewriting Systems,” Technical Report 87-6, Department of Computer Science, State University of New York, Albany, N.Y. 12222.

    Google Scholar 

  13. S. MacLane and G. Birkhoff, Algebra, The Macmillan Company, New York, 1967.

    Google Scholar 

  14. M. H. A. Newman, “On theories with a combinatorial definition of ‘equivalence',” Annals of Mathematics 43/2 (1942), 223–243.

    Google Scholar 

  15. G. Peterson and M. Stickel, “Complete sets of reductions for some equational theories,” Journal of the Association for Computing Machinery, 28 (1981), 233–264.

    Google Scholar 

  16. M. Stickel, “A unification algorithm for associative-commutative functions,” Journal of the Association for Computing Machinery, 28 (1981), 423–434.

    Google Scholar 

  17. F. Winkler and B. Buchberger, “A Criterion for Eliminating Unnecessary Reductions in the Knuth-Bendix Algorithm,” Colloquia Mathematica Societatis János Bolyai 42, Algebra, Combinatorics and Logic in Computer Science, Györ, Hungary, 1983.

    Google Scholar 

  18. H. Zhang and D. Kapur, “Consider Only General Superpositions in Completion Procedures,” Lecture Notes in Computer Science 355, Rewriting Techniques and Applications, RTA-89, Springer-Verlag, 1989, 511–527.

    Google Scholar 

  19. H. Zhang and J.-L. Remy, “Contextual Rewriting,” Lecture Notes in Computer Science 202 Rewriting Techniques and Applications, edited by Jean-Pierre Jouannaud, 1985, 46–62.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. McDonnell Douglas Corporation, 1065165, P. O. Box 516, 63166, St. Louis, Missouri

    Gerald E Peterson

Authors
  1. Gerald E Peterson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mark E. Stickel

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Peterson, G.E. (1990). Complete sets of reductions with constraints. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_101

Download citation

  • DOI: https://doi.org/10.1007/3-540-52885-7_101

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52885-2

  • Online ISBN: 978-3-540-47171-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation