Knuth–Bendix Completion

A procedure applied to a presented rewriting system that attempts to produce a confluent (complete) term-rewriting system by orienting relations into rewrite rules under a chosen reduction ordering and adding consequences obtained from critical overlaps until no unresolved critical pairs remain or the process diverges.

An algorithmic procedure taking a set of rewrite rules (or relations) together with a well-founded reduction ordering and attempting to extend the rule set by adding consequences (resolving critical pairs) so as to produce a confluent (and terminating) rewriting system that decides word equality in the presented algebra when successful.