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:

• String rewriting
• Term rewriting
• Graph rewriting
• Ground rewriting
• Higher-order rewriting
• Conditional rewriting
• Priority rewriting
• Constrained rewriting
• Parallel rewriting
• Infinite rewriting

The field pretty cleanly splits in two directions:

• Programming Languages
  • Confluence
  • Termination
  • Semantics
  • Normalization strategies
  • Combinatory logic
  • Lambda calculi
  • Functional and logic programming languages
• Automated Deduction
  • Symbolic and algebraic computation
  • Decision procedures
  • Completion techniques
  • Rewriting-based theorem proving
  • Equation solving
  • Unification and matching
  • Constrained deduction
  • Constraint solving
  • Parallel deduction

---

Realized by Nachum Dershowitz and Laurent Vigneron.