Knuth–Bendix completion algorithm
The Knuth–Bendix completion algorithm (named after Donald Knuth and Peter Bendix) is a semi-decisionalgorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it effectively solves the word problem for the specified algebra.
Buchberger's algorithm for computing Gröbner bases is a very similar algorithm. Although developed independently, it may also be seen as the instantiation of Knuth–Bendix algorithm in the theory of polynomial rings.
For a set E of equations, its deductive closure () is the set of all equations that can be derived by applying equations from E in any order. Formally, E is considered a binary relation, () is its rewrite closure, and () is the equivalence closure of (). For a set R of rewrite rules, its deductive closure ( ∘ ) is the set of all equations than can be confirmed by applying rules from R left-to-right to both sides until they are literally equal. Formally, R is again viewed as binary relation, () is its rewrite closure, () is its converse, and ( ∘ ) is the relation composition of their reflexive transitive closures ( and ).
...
Wikipedia