Efficient ground completion

An O(n log n) algorithm for generating reduced sets of ground rewrite rules equivalent to a set of ground equations E
  • Wayne Snyder
Regular Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 355)


We give a fast method for generating reduced sets of rewrite rules equivalent to a given set of ground equations. Since, as we show, reduced ground rewrite systems are in fact canonical, this is essentially an efficient Knuth-Bendix procedure for the ground case. The method runs in O(n log n), where n is the number of occurrences of symbols in E. We also show how our method provides a precise characterization of the (finite) collection of all reduced sets of rewrite rules equivalent to a given ground set of equations E, and prove that our algorithm is complete in that it can enumerate every member of this collection. Finally, we show how to modify the method so that it takes as input E and a total precedence ordering on the symbols in E, and returns a reduced rewrite system contained in the lexicographic path ordering generated by the precedence.


Word Problem Theorem Prove Ground Term Quotient Graph Equational Mating 
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.

5 References

  1. [1]
    Ackermann, W., Solvable Cases of the Decision Problem. North-Holland, Amsterdam (1954).Google Scholar
  2. [2]
    Andrews, P.B., “Theorem Proving via General Matings,” JACM 28:2 (1981) 193–214.Google Scholar
  3. [3]
    Bachmair, L. Proof Methods for Equational Theories, Ph.D thesis, University of Illinois, Urbana Champaign, Illinois (1987).Google Scholar
  4. [4]
    Bachmair, L., Dershowitz, N., and Hsiang, J., “Orderings for Equational Proofs,” In Proc. Symp. Logic in Computer Science, Boston, Mass. (1986) 346–357.Google Scholar
  5. [5]
    Dauchet, M., Tison, S., Heuillard, T., and Lescanne, P., “Decidability of the Confluence of Ground Term Rewriting Systems,” LICS'87, Ithaca, New York (1987) 353–359.Google Scholar
  6. [6]
    Dershowitz, N., “Termination of Rewriting,” Journal of Symbolic Computation 3 (1987) 69–116.Google Scholar
  7. [7]
    Dershowitz, N., “Completion and its Applications,” Proceedings of CREAS, Lakeway, Texas (May 1987).Google Scholar
  8. [8]
    Downey, P.J., Samet, H., and Sethi, R., “Off-line and On-line Algorithms for Deducing Equalities,” POPL-5, Tucson, Arizona (1978).Google Scholar
  9. [9]
    Downey, P.J., Sethi, R., and Tarjan, E.R., “Variations on the Common Subexpressions Problem,” JACM 27:4 (1980) 758–771.Google Scholar
  10. [10]
    Gallier, J.H. Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, New York (1986).Google Scholar
  11. [11]
    Gallier, J.H., Raatz, S., and Snyder, W., “Theorem Proving using Rigid E-Unification: Equational Matings,” LICS'87, Ithaca, New York (1987) 338–346.Google Scholar
  12. [12]
    Gallier, J., Narendran, P., Raatz, S., and Snyder, W., “Theorem Proving using Equational Matings and Rigid E-Unification,” submitted to JACM (1988).Google Scholar
  13. [13]
    Gallier, J.H., Narendran, P., Plaisted, D., and Snyder, W., “Rigid E-Unification is NP-complete,” LICS'88, Edinburgh, Scotland (July 1988)Google Scholar
  14. [14]
    Gallier, J.H., Narendran, P., Plaisted, D., and Snyder, W., “Rigid E-Unification: NP-Completeness and Applications to Equational Matings,” submitted to Information and Computation (1988).Google Scholar
  15. [15]
    Gallier, J.H., Narendran, P., Plaisted, D., Raatz, S., and Snyder, W., “Finding Canonical Rewriting Systems Equivalent to a Finite Set of Ground Equations in Polynomial Time,” CADE-9, Argonne, Ill. (1988) (Journal version submitted to JACM (1988).)Google Scholar
  16. [16]
    Huet, G., “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,” JACM 27:4 (1980) 797–821.Google Scholar
  17. [17]
    Huet, G. and Oppen, D. C., “Equations and Rewrite Rules: A Survey,” in Formal Languages: Perspectives and Open Problems, R. V. Book (ed.), Academic Press, NY (1982).Google Scholar
  18. [18]
    Huet, G., Lankford, D., “On the Uniform Halting Problem for Term Rewriting Systems,” Rapport de Recherche 283 (March 1978).Google Scholar
  19. [19]
    Kamin, S., and Levy, J.-J., “Two Generalizations of the Recursive Path Ordering,” unpublished note, Department of Computer Science, University of Illinois, Urbana, IL.Google Scholar
  20. [20]
    Kozen, D., “Complexity of Finitely Presented Algebras,” Technical Report TR 76-294, Department of Computer Science, Cornell University, Ithaca, NY (1976).Google Scholar
  21. [21]
    Lankford, D.S., “Canonical Inference,” Report ATP-32, University of Texas (1975)Google Scholar
  22. [22]
    Metivier, Y., “About the Rewriting Systems Produced by the Knuth-Bendix Completion Algorithm,” Information Processing Letters 16 (1983) 31–34.Google Scholar
  23. [23]
    Nelson G., and Oppen, D. C., “Fast Decision Procedures Based on Congruence Closure,” JACM 27:2 (1980) 356–364.Google Scholar
  24. [24]
    Oyamaguchi, M., “The Church-Rosser Property for Ground Term-Rewriting Systems is Decidable,” TCS 49 (1987) 43–79.Google Scholar
  25. [25]
    Rosen, B., “Tree-Manipulating Systems and Church-Rosser Theorems,” JACM 20 (1973) 160–187.Google Scholar
  26. [26]
    Shostak, R., “An Algorithm for Reasoning about Equality,” CACM 21:7 (July 1978) 583–585.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • Wayne Snyder
    • 1
  1. 1.Department of Computer ScienceBoston UniversityBoston

Personalised recommendations