Abstract :
Knuth-Bendix for strings, when applied to a presentation for a group G, often diverges. In this paper we develop a Knuth-Bendix procedure for equational term rewriting which can find an infinite, complete presentation for G in certain cases where previous procedures fail. These presentations yield an efficient solution of the word problem for G in the same way as finite ones, by reducing any word to a unique normal form. Our presentations consist of finitely many families, each of which is parameterized by a single term rewrite rule. The parameters are formal variables which occur in exponents, and take all positive integer values. We give an example of a group which is not FP∞, hence which has no finite complete rewrite system, and is not automatic, but which has a complete presentation in our sense.
