A set `E` of equations defines an *equational theory*, which is the set
of equations that can be derived from `E` by substituting equals for equals.
More generally, a set of equations and
rewrite rules defines an equational
theory, which is that obtained by considering the rewrite rules as equations.
A major purpose of the Knuth-Bendix completion procedure is to provide a
decision procedure (reduction to normal form) for the question of whether
equations are in the equational theory of a given system of equations and
rewrite rules.