In this paper we present a generalization of the Knuth-Bendix procedure for generating a complete set of reductions modulo an equational theory. Previous such completion procedures have been restricted to equational theories which generate finite congruence classes. The distinguishing feature of this work is that we are able to generate complete sets of reductions for some equational theories which generate infinite congruence classes. In particular, we are able to handle the class of equational theories which contain the associative, commutative, and identity laws for one or more operators.

We first generalize the notion of rewriting modulo an equational theory to include a special form of conditional reduction. We are able to show that this conditional rewriting relation restores the finite termination property which is often lost when rewriting in the presence of infinite congruence classes. We then develop Church-Rosser tests based on the conditional rewriting relation and set forth a completion procedure incorporating these tests. Finally, we describe a computer program which implements the theory and give the results of several experiments using the program.


Computer Science


This report is substantially the Ph.D. dissertation of the first author, completed, July 1988.

Keywords and Phrases

Complete Sets of Reductions; Knuth-Bendix Procedure; E-Completion; E-Unification; Conditional Reductions; Finite Termination Property; Church-Rosser Property

Report Number


Document Type

Technical Report

Document Version

Final Version

File Type





© 1988 University of Missouri--Rolla, All rights reserved.

Publication Date

July 1988