Equational reasoning is an important component in symbolic algebra, automated deduction, high-level programming languages, program verification, and artificial intelligence. Reasoning with equations involves deriving consequences of given equations and finding values for variables that satisfy a given equation. Rewriting is a very powerful method for dealing with equations.

Directed equations, called rewrite rules, are used to replace equals by equals, but only in the indicated direction. The theory of rewriting centers around the concept of normal form, an expression that cannot be rewritten any further. Computation consists of rewriting to a normal form; when the normal form is unique, it is taken as the value of the initial expression. When rewriting equal terms always leads to the same normal form, the set of rules is said to be convergent and rewriting can be used to check for equality.

Rewriting comes in various flavors, including: The field pretty cleanly splits in two directions:


Realized by Nachum Dershowitz and Laurent Vigneron.