The class of finitely presented groups defined by finite rewrite systems provide a Magma level interface to Derek Holt's KBMAG programs, and specifically to the Knuth--Bendix completion procedure for groups defined by a finite (monoid) presentation. Much of the material in this chapter is taken from the KBMAG documentation [Hol97]. Familiarity with the Knuth--Bendix completion procedure is assumed. Some familiarity with KBMAG would be beneficial.
A rewrite group G is a finitely presented group in which equality between elements of G, called words or strings, may be decidable via a sequence of rewriting equations, called reduction relations, rules, or equations. In the interests of efficiency the reduction rules are codified into a finite state automaton called a reduction machine. The words in a rewrite group G are ordered, as are the reduction relations of G. Several possible orderings of words are supported, namely short-lex, recursive, weighted short-lex and wreath-product orderings. A rewrite group can be confluent or non-confluent. If a rewrite group G is confluent its reduction relations, or more specifically its reduction machine, can be used to reduce words in G to their irreducible normal forms under the given ordering, and so the word problem for G can be efficiently solved.
The family of all rewrite groups forms a category. The objects are the rewrite groups and the morphisms are group homomorphisms. The Magma designation for this category of groups is GrpRWS. Elements of a rewrite group are designated as GrpRWSElt.
A rewrite group G is constructed in a three-step process: