Motivation

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.