• Enno Ohlebusch


Equations were among the first mathematical achievements of mankind. For example, they appear in old Babylonian texts written in cuneiform characters that date back to the third millennium B.C. This is not surprising because equational reasoning (replacing equals with equals, that is) occurs frequently in day-to-day life. For example, in calculating a simple arithmetic expression like (3 + 3) * 6, one first uses the equation 3 + 3 = 6 to replace the expression or the term (3 + 3) * 6 with 6*6. In a second step this term further rewrites to 36, the result of the computation. In calculating the intuitively simplest term equal to (3 + 3) * 6, no one would use the equation 3 + 3 = 6 to replace the term (3 + 3) * 6 with the term (3 + 3) * (3 + 3). In other words, the equation 3 + 3 = 6 is used as a rewrite rule: the left-hand side can be replaced with the right-hand side, but not vice versa. This one-directional replacement of equals with equals is what distinguishes term rewriting from equational logic.


Normal Form Mathematical Achievement Coffee Bean Critical Pair Black Bean 
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.

Copyright information

© Springer Science+Business Media New York 2002

Authors and Affiliations

  • Enno Ohlebusch
    • 1
  1. 1.Research Group in Practical Computer Science, Faculty of TechnologyUniversity of BielefeldBielefeldGermany

Personalised recommendations