Standard Completion

Abstract

Knuth and Bendix (1970) proposed a procedure that attempts to transform a given set of equations into a convergent rewrite system. This completion procedure must be supplied with a reduction ordering, which determines the direction in which an equation is to be oriented into a rewrite rule. It deduces new equations by a process called superposition. An intriguing feature of the procedure is that rewrite rules can be used to simplify other, already deduced equations. Terms can therefore be kept in fully simplified form and redundant equations can be discarded. Deduction and simplification are the two main components of completion. While simplification accounts for the practicality of completion, it also complicates the task of verifying that a procedure is correct (i. e., does in fact produce a convergent set of equations).