# Introduction

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 [[Holt, 1997](../../references.md#cite-kbmag)]. Familiarity with the Knuth–Bendix completion procedure is assumed. Some familiarity with KBMAG would be beneficial.

## Terminology

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 Category of Rewrite Groups

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`.

## The Construction of a Rewrite Group

A rewrite group $G$ is constructed in a three-step process:

**(i)**
We construct a free group $FG$.

**(ii)**
We construct a quotient $F$ of $FG$.

**(iii)**
We create a monoid presentation of $F$ and then run a Knuth–Bendix completion procedure on this presentation to create a rewrite group $G$.

The Knuth–Bendix procedure may or may not succeed. If it fails the user may need to perform the above steps several times, manually adjusting the parameters to the Knuth–Bendix procedure. If it succeeds then the rewrite system constructed will be confluent.