Handbook of Automated Reasoning

6 Completion

The impractical, “British Museum” approach to constructing a convergent system for a given equational theory E would be to generate all possible sets of equational consequences of E, orient as many as possible according to some given reduction ordering, and check each subset of the rules for completeness (all E follows) and confluence (all critical pairs between the resultant rules resolve). As a practical matter, a method, called completion, is used, which converts unresolved critical pairs into rewrite rules. Completion uses a reduction ordering to orient equations, rewriting to simplify rules and equations, and the encompassment ordering to determine which of two rules is more general, and hence preferred. Knuth and Bendix ...