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.