Normalization via Rewrite Closures

  • L. Bachmair
  • C. R. Ramakrishnan
  • I. V. Ramakrishnan
  • A. Tiwari
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1631)


We present an abstract completion-based method for finding normal forms of terms with respect to given rewrite systems. The method uses the concept of a rewrite closure, which is a generalization of the idea of a congruence closure. Our results generalize previous results on congruence closure-based normalization methods. The description of known methods within our formalism also allows a better understanding of these procedures.


Normal Form Inference Rule Transformation Rule Ground Term Detection Rule 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    L. Bachmair. Canonical equational proofs. Birkhäuser, Boston, 1991.Google Scholar
  2. [2]
    L. Bachmair and N. Dershowitz. Equational inference, canonical proofs, and proof orderings. JACM, 41:236–276, 1994.MATHCrossRefMathSciNetGoogle Scholar
  3. [3]
    L. P. Chew. An improved algorithm for computing with equations. In 21st Annual Symposium on Foundations of Computer Science, 1980.Google Scholar
  4. [4]
    L. P. Chew. Normal forms in term rewriting systems. PhD thesis, Purdue University, 1981.Google Scholar
  5. [5]
    N. Dershowitz and J. P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science (Vol. B: Formal Models and Semantics), Amsterdam, 1990. North-Holland.Google Scholar
  6. [6]
    D. Kapur. Shostak’s congruence closure as completion. In H. Comon, editor, Proc. 8th Intl. RTA, pages 23–37, 1997. LNCS 1232, Springer, Berlin.Google Scholar
  7. [7]
    J. W. Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1, chapter 6, pages 2–116. Oxford University Press, Oxford, 1992.Google Scholar
  8. [8]
    G. Nelson and D. Oppen. Fast decision procedures based on congruence closure. JACM, 27(2):356–364, 1980.MATHCrossRefMathSciNetGoogle Scholar
  9. [9]
    D. J. Sherman and N. Magnier. Factotum: Automatic and systematic sharing support for systems analyzers. In Proc. TACAS, LNCS 1384, 1998.Google Scholar
  10. [10]
    R. M. Verma. A theory of using history for equational systems with applications. JACM, 42:984–1020, 1995.MATHCrossRefGoogle Scholar
  11. [11]
    R. M. Verma and I. V. Ramakrishnan. Nonoblivious normalization algorithms for nonlinear systems. In Proc. of the Int. Colloquium on Automata, Languages and Programming, New York, 1990. Springer-Verlag.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • L. Bachmair
    • 1
  • C. R. Ramakrishnan
    • 1
  • I. V. Ramakrishnan
    • 1
  • A. Tiwari
    • 1
  1. 1.Department of Computer ScienceSUNY at Stony BrookUSA

Personalised recommendations