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.