Complete Sets of Reductions for Some Equational Theories

Abstract

An extenston of the Knuth-Bendix algorithm for finding complete sets of reductions is described. The extension is intended to handle equational theories which can be split into two parts, R and T, such that each equation m R can be construed as a reduction and T represents an equational theory for which a finite, complete umficat~on algorithm ~s known. The extension ts demonstrated in the case when T is the theory of a fimte number of associaUve and commutatwe functions and to which the extension is presently restricted An tmplementatlon of the extended Knuth-Bendtx algorithm has produced complete sets of reductions for free commutattve groups, commutative rings wtth umt, and distributive lattices.