KB(rws)
Run the external Knuth-Bendix program on the rewriting system rws.
KB returns true if it finds a confluent rewriting system and
otherwise false. In either case, if it halts normally, then it will
update rws by changing the equations field, which contains a list
of the rewriting rules, and by appending a finite state automaton
rws.reductionFSA that can be used for word reduction, and the
counting and enumeration of irreducible words.
All control parameters (as defined in the preceding section) should be
set before calling KB. In the author's experience, it is usually
most helpful to run KB with the verbose flag rws.verbose set, in
order to follow what is happening. KB will halt either when it
finds a finite confluent system of rewriting rules, or when one of the
control parameters (such as rws.maxeqns) requires it to stop. The
program can also be made to halt and output manually at any time by
hitting the interrupt key (normally ctr-C) once. (Hitting it twice
has unpredictable consequences, since GAP may intercept the
signal.)
If KB halts without finding a confluent system, but still manages to
output the current system and update rws, then it is possible to use
the resulting rewriting system to reduce words, and count and
enumerate the irreducible words; it cannot be guaranteed that the
irreducible words are all in normal form, however. It is also possible
to re-run KB on the current system, usually after altering some of
the control parameters. In fact, is some more difficult examples, this
seems to be the only means of finding a finite confluent system.
GAP 3.4.4