Usage Information for automata and Related Programs

This section lists detailed usage information for the executable files included in MAF that work with rewriting systems. However, it does not include information about any of the utilities that work directly with FSA files. Their usage is described in "MAF Finite State Automata Utilities".

This section is divided into several parts:

If an executable file included with MAF is not listed either here or in "MAF Finite State Automata Utilities", you can safely assume it is one of the more obscure utilities retained for compatibility with KBMAG. If you are curious, you can, as is the case with all MAF utilities, run them with no command line arguments, and they will report their intended purpose and usage details. Alternatively consult the source code.

Input and Output files, Piping and Redirection.

Most MAF utilities can read their input file either from an ordinary disk file, or from the computer's "standard input" (henceforth called stdin). The latter is always enabled through the use of the -i command line option, which must appear before any command line argument that would otherwise be interpreted as the name of an input file. Similarly, programs can send their output either to an ordinary disk file or to "standard output" (henceforth called stdout). Usually output is sent to a filename derived from the name of the input file unless an explicit filename is given for the output filename. For those programs that send can send output to stdout, this is enabled by using the -o command line option. Generally speaking it is better to specify an explicit filename (or ".") rather than sending output to a redirected stdout, because in the latter case you won't be able to see any of the messages that the program may want to produce while it is running, and that inform you of its progress so far. However, the ability to read from stdin and write to stdout does mean that MAF utilities can be used as pipes.

For example, you could minimise and sort an FSA effectively in a single command using a command line such as the following:

fsamin some_fsa -o | fsabfs -i some_fsa.canonical

Alternatively you could rely on the default output filename feature to achieve similar results, like this:

fsamin some_fsa
fsabfs some_fsa.min

In this case the final "canonical" fsa is now called some_fsa.min.bfs.

Unfortunately you can't use the default output filename with the -i option. If you do, output will just be sent to stdout anyway, but the output is likely to be invalid, because the progress messages will be mixed up with the correct output. Normally MAF caters for this by adjusting the format of the diagnostics so that they appear as comments in the ouput, and so the output is still valid, but using the combination -i and -o together will prevent this from happening.

Some of the more complex programs, notably automata itself, only accept input from a file, and can only send output to files. This is usually because the program generates several separate output files, or because later use of their output files also requires the original input file.

This is one area in which MAF is not entirely compatible with KBMAG, because many KBMAG programs will normally automatically read stdin if no input file is given, and in this case will automatically output to stdout. Also in KBMAG output files cannot usually be given names, and the name will be similar to the default output filename in MAF. It is hoped that this will not cause problems for users familiar with KBMAG. If it does, then it should be possible to remove the incompatibility by the simple expedient of renaming the problematic MAF program and creating a small script program which accepts the equivalent kbmag command line and then invokes the renamed program. In general MAF executables can replace KBMAG executables with the same name in GAP.

Command Line Options

Most MAF utilities accept a good number of "command line options", though it is the author's intention that you should not actually have to use many of these most of the time. In general options can be specified anywhere on the command line, and in any order, though it is usually a good idea to put all such options before any filenames. Command line options always begin with a '-' character, and are always separate words: you cannot combine several single letter options into one longer option, as is possible with some packages. In fact there are relatively few single letter command line options, and most of these are only included for compatibility with KBMAG. Most command line options in MAF are ordinary English words, intended to describe the purpose or effect of the option. A few command line options require a parameter, often a number. This must always be specified immediately after the option itself but separated from it by at least one space.

Standard Options

Many command line options are present in many, most, or even every, individual MAF program, and have the same meaning wherever they occur. To avoid repeating them over and over again, we list them here. Some of these options are "compatibility" options. This means that MAF programs accept them as valid options, but does nothing with them other than to parse them. These are options that are used in KBMAG but which are either not needed or not yet implemented in MAF. We also describe the use of the "." filename again, and the use of the -i option.

loglevel -v

The verbose option. Status information on progress of programs is sent to stdout. In general status information is generated approximately once per second. -v is on by default, but is provided as an explicit option for compatibility with kbmag. -verbose, -vv and -v all usually have the same effect. The status information can often give you a good idea as to whether the program you are running is likely to succeed or not.


Status information is only sent to stdout at significant points in the execution of programs. There is no "comfort output" to indicate that a lengthy task is proceeding normally. Specifying "-quiet" makes the level of output similar to what is generated by KBMAG without -v, though the detailed diagnostics are (of course) different.


No status information at all is produced. Note that there is generally no need to use this option, even if you are sending the program's "proper" output to stdout and using this as the input to another program, because in this case all diagnostic information will be prefixed with "#" characters, so that if the other program is expecting GAP format input it will ignore the diagnostics as comments.

compatibility -fKBMAG uses this to modify the operation of functions that build and minimise FSAs. It is possible that this option will be implemented in MAF in future.

KBMAG uses these to control the size of "hash tables". In MAF hash tables are adjusted automatically.

-ip d
-ip s

KBMAG uses these options to specify the expected format of an input FSA. MAF will happily process an FSA in any format and does not need to be told in advance what format it is getting.

Format options -dense or -op d
-op s
or -sparse

In programs that generate FSAs one of these options can be used to specify the format in which the transition table is stored in output files. -dense or -op d selects "dense" format, and -sparse or -op s selects "sparse" format. MAF usually uses dense format for one-variable automata, and sparse format for two-variable automata, but this is not always the case. Neither format is particularly legible to humans. Sparse format is perhaps marginally easier to read, especially for FSAS with many possible transitions from each state, but dense format perhaps gives a better subjective impression of what the FSA is like. The printing format has no necessary connection with the in memory format of the FSA.

It is not advisable to use these options in automata itself, and particularly not -dense/-op d because it applies to all the automata generated: MAF does not support the various variations on "-op" present in KBMAG. You can easily change the format of an FSA later on using fsaprint.

-csn or -comment

In programs that generate FSAs this option can be used to request that the transition table is output with comments indicating the state number to which the each set of transitions applies. MAF comments every fifth state, with the comment appearing as a separate line before the transitions. This improves the readablity of FSA files.


In programs that generate FSAs the transition table is output with comments indicating whether the state is initial or accepting, and if not the shortest path from an initial state and to an accepting state is shown.


In programs that generate FSAs the transition table of product FSAs is annotated with comments which make it easier for a human to read the transition table. Usually you will only want to use either of the annotation options with the program fsaprint since they increase the size of output files considerably.

input_file-i| input_file

When ever you see the text -i | input_file in a program usage summary, it means that the program can either take its input from a file, in which case you replace input_file by a suitable filename, or it can take its input from the stdin, in which case the input will normally come from another MAF programs's stdout. You cannot use the -i option more than once on any command line, and you can only use it in place of the filename next to which it is shown in the program description, and you cannot use it at all if it is not desribed explicitly in the usage information for the program. On command lines, the -i option must come before where MAF would be expecting the relevant filename. MAF will usually notice, and flag as a usage error, if you have tried using the -i option too late.

output_file-o | output_file

As already mentioned MAF utilities that generate only one file send output to a filename based on the input file by default. MAF therefore uses the following scheme consistently in all utilities that produce only one file:

  • If the -o option is specified, or no filename, output is sent to stdout and diagnostic output is modified so that all diagnostic lines are preceded by #.
  • If no output filename is given then a filename is generated using the input file_name and a suffix in a scheme similar to KBMAG,
  • Otherwise the output filename given is treated as a complete filename.

Even if a program does not support the -i command line option, if it still supports output to stdout its optional output filename will always be shown as output_file in usage information, both in this document and in the usage information that appears when you run the program without any options.

Useful Programs in MAF


automata [options] groupname

Compute the finite state automata that constitute the automatic structure of a confluent rewriting system, or a shortlex automatic group or coset system and various associated automata. Input is taken from the file groupname, which should contain a declaration of a record defining a rewriting system, in the format described in the Introduction.


Please also refer to Useful Command Line options. The information geiven there is not repeated here.


This option is applies when coset systems are being analysed. If automata finds at some stage that there are only finitely many irreducible words of the form _Hw (which implies that |G:H| is finite), then automata stops the Knuth Bendix phase as soon as convenient, without the system necessarily being confluent. At this stage, it is guaranteed that all words of the form _Hw reduce under the system to _Hw′ (or h_Hw′), where w′ is the correct minimal word that lies in in the coset _Hw. In other words, it reduces cosets of H correctly, even though it may not reduce all G-words or H-words correctly. However, if H-generators are present, then it is also guaranteed that the H-equations will form a presentation of H (although not necessarily a confluent one). The index of H in G will be equal to the number of irreducible words of form _Hw, and will be printed as a message by automata before it halts.

Conversely, if the index of H in G is finite, and the -detect-finite-index option is specified, then it can be proved that the algorithm employed will eventually halt, although it may take a long time. So it can be used as an alternative to Todd-Coxeter coset enumeration for calculating |G:H|, and to the modified Todd-Coxeter method of calculating subgroup presentations. However, it does appear that the Todd-Coxeter based methods are somehat more efficient in most examples. However, for very difficult presentations MAF is sometimes able to find that a subgroup has finite index when coset enumeration fails. Subgroup presentations calculated by MAF are usually less redundant than those calculated by applying the Reidermeister Schreier algorithm to a coset table.


This is a second, more aggressive, option with roughtly the same meaning as -detect_finite_index. However, the first option will not prevent an automatic structure for a non-finite index from being found, whereas -prove_finite_index most probably will. With this option MAF behaves somewhat like a coset enumerator, in that it will create as many coset equations as it possibly can, as quickly as it can. Long coset equations will not be pooled as they normally would be.


This option is only relevant when a coset system with named subgroup generators is being processed. As previously mentioned the h-words that appear on the RHS of coset equations can be extremely long. When this option is used, MAF does not cound the h-word part of the RHS in the size of the equation, so that coset equations will be more likely to be inserted into the tree rather than being pooled.


This option is only relevant when a coset system with named subgroup generators is being processed. When this option is used MAF will not ever perform Knuth Bendix expansion on equations in the h-words alone. This means it can afford to allow all h-equations that are created into the tree immediately, even though they may be very long. Somewhat paradoxically, this seems to improve the stability of MAF considerably with this type of coset system. In fact both this option and the previous one will probably be made the defaults in future.

Additional Logging Options

The following options can be used to follow MAF's chain of reasoning in its analysis of a rewriting system. Neither of the first two options, particularly not the second, is to be recommended for other than the smallest examples, because the volume of output produced will be very high.


The verbose-equations option. Each new equation is printed as it is found.


The very verbose-equations option. Not only is each new equation printed out, so is an outline proof that it is true.


The verbose word-differences option. In addition to MAF's normal output, each new word-difference found is printed to stdout, together with the equation from which it was calculated.


gpgeowa [loglevel] [format] [reduction_method] [-near | n] groupname

This program attempts to construct the geodesic word-acceptor of a word-hyperbolic group, after the automatic structure has been calculated. In theory, it works whenever the group is word-hyperbolic, so if it succeeds, then the group has been proved to have this property (due to a result proved by Panos Papasoglu), although it does not provide an estimate of the hyperbolic constant.

If the group is not word-hyperbolic, then gpgeowa will not terminate.

It is assumed that the file groupname contains a rewriting system defining a shortlex automatic group, and that automata has already been run successfully on this file.

Input is from groupname.wa, groupname.diff2, and from one of the automata capable of performing word reduction. Output (when successful) is to the three files groupname.geowa, which contains the geodesic word-acceptor, groupname.geopairs, which contains a two-variable automaton whose language consists of all pairs of equal geodesic words in the group generators, and groupname.geodiff, which contains a two-variable word-difference machine, consisting of the word-differences and transitions necessary for constructing groupname.geopairs.

If the -near option is specified, then an additional 2-variable automaton is output to groupname.near_geopairs.This automaton accepts all pairs of words u and v such such that v is geodesic and ux==v for x either the identity or some generator.

MAF uses a different algorithm from KBMAG to calculate geodesic automata.


gpsubwa [loglevel] [format] [-diff1cos/-diff2cos] groupname [subsuffix]

gpsubwa attempts to compute a subgroup word-acceptor for the subgroup H of the automatic group G (whose automatic structure has previously been computed), where the rewriting system for G is defined in groupname, and the generators for H are defined in the file, groupname.subsuffix, where subsuffix defaults to sub. See Subgroup Files for information on the format of the latter file.) The computed automaton is output to the file groupname.cossuffix.subwa. This is different from KBMAG which uses the name groupname.subsuffix.wa.

gpsubwa requires the word-acceptor and general multiplier for an automatic structure of G, which it inputs from the files groupname.wa and These need to be computed first by running automata or its constituents. It also requires word-reduction automata for G and for cosets of H in G, as described above. These are input, respectively, from groupname.diff2 and groupname.cosname.kbprog by default, but these defaults may be changed by using the appropriate options (see below). Here cosname is derived from subsuffix by substituting the string cos for sub as described in Chapter "Subgroup and Coset Files".

automata and autcos will normally attempt to create the subgroup word-acceptor as the last thing they do. However, if you forgot to first find the automatic structure for the group itself, this stage is skipped, or you may have used an option to prevent this acceptor from being calculated, so it is sometimes useful to be able to do this separately. It is also sometimes possible to create a subgroup word-acceptor even when MAF could not find an automatic coset structure, and in these circumstances also you will need to run gpsubwa separately.



Take the input automaton for coset word-reduction of words in G as coset representatives of H in G from groupname.cosname.midiff1 or groupname.cosname.midiff2, rather than from groupname.cosname.kbprog.


gpvital calculates a new presentation for a group whose automatic structure has already been computed. The presentation is usually based on the correct primary word difference machine (the .diff1c FSA), and is in some sense a canonical presentation for the particular generating set and word-ordering method used in the rewrting system. In principle there is an axiom which proves the necessity of each transition in this word-difference machine. However, MAF will usually simplify the new presentation somewhat by eliminating axioms that are obvious consequences of earlier ones. This simplification can be prevented by use of the -raw option, or you can ask MAF to make a more determined effort to eliminate unnecessary axioms by using the -eliminate option.

The -axioms option will cause the original axiom set to be included first. This option may be of interest when you have finally succeeded in finding the automatic structure for a highly pathological group presentation: any extra axioms in the new presentation will normally be equations that are very hard to prove using the original axiom set, and the automatic structure will usually be much easier to compute using the new presentation.


reduce [loglevel] [-steps] [reduction_method] rwsname [-i | -read filename | word][output_file]

where reduction_method is one of the following values: -kbprog,-gm,-diff2c,-diff1c,-diff2, -pdiff2, -pkbprog, -pdiff1

This program can be used to reduce words to their normal form in the ordering specified in file rwsname. It is assumed that automata has previously run, and that is has output at least one FSA which makes at least provisional word reduction possible. If not, or if you specify that reduce should use an automaton that is not available, then reduce will exit with an error message and error level.

reduce reduces words using one of the automata produced by automata. The reductions will always be correct in the sense that the output word will represent the same element as the input word. If automata has completed sucessfully, then at least one of the the first five automatons in the list of values that can be specified for reduction_method will exist, and reduce will use this automaton to perform the word reduction. It can therefore be used to solve the word problem in the monoid. If automata produced only provisional output, then there will be some pairs of words which are really equal as elements, but which reduce to distinct words, and so this program cannot be used to solve the word problem.

If the -steps option is specified MAF will apply one reduction at a time to the word and output each word.

The KBMAG option -mrl maxreducelen is accepted, but ignored. Throughout MAF, words are limited to a length of MAX_WORD symbols, which currently equals 65533 symbols.

An output_file may only be specified if the -read filename option has been used. If the -i option is used then the program will display a prompt and allow words to be input interactively. Words must be terminated with a ',' or a ';' when you want to quit the program. On most operating systems it will be necessary to press enter after the ',' or ';' character.

If the -read option is specified, then the input file should be a GAP list using the following syntax:

words := 
  word1, word2, ... wordn
Each word should follow the same rules for input as are used in MAF's usual input files.


gpmult [loglevel] [format] [-cos] [-pres | -2 | -sub | -word expression] groupname [subsuffix]

This program assumes that the shortlex automatic structure has already been created for the group, i.e. that has been created successfully. gpmult can compute various additional multiplier automata which may sometimes be useful:


gporder [loglevel] [-steps] [reduction_method] rwsname [-i | -read filename | word]

where reduction_method is one of the following values: -kbprog,-gm,-diff2c,-diff1c,-diff2, -pdiff2, -pkbprog, -pdiff1

This program can be used to find the order of torsion elements. It is assumed that automata has previously run, and that is has output at least one FSA which makes at least provisional word reduction possible. If not, or if you specify that gporder should use an automaton that is not available, then gporder will exit with an error message and error level.

gporder reduces successive powers of the word(s) until it reaches the identity word. If the group is infinite and a word acceptor is available MAF will also check, for each power it computes, whether the word-acceptor will accept that word infinitely often - which proves the element is not a torsion element. If the maximum wordlength is exceeded before either of these things happens then the program will crash. The program does not yet attempt to use information about the order of a finite group to work more efficiently, and the method used to detect that an element is not a torsion-element is not yet as good as it could be.

If an input file in GAP format is supplies gporder will calculate the orders of all the words in the list and output a list consisting of the words and the corresponding order.


isconjugate [loglevel] [reduction_method] groupname word1 [word2]

isconjugate can be used to attempt to determine either whether two words are conjugates (if two words are specified on the command line), or the set of words that are conjugate to the given word (if only one word is specified). If requires that automata or a similar program has computed an automaton that allows word-reduction to take place.

When two words are specified isconjugate will attemptto find the conjugacy class of each word, and stop if it finds that these have a common element, at which point it can compute an element u such\nthat word1^u=u^-1*word1*u = word2. The return value is 0 if a conjugating\nelement is found, or 2 if the group is finite and there is no such element, or the group is infinite but either word1 or word2 have only finitely many conjugates and are not conjugate. In the case where both conjugacy classes are infinite and different isconjugate will run until it runs out of memory and crashes or it tries to create a word that is longer than the maximum word length allowed. isconjugate is very simple-minded, and there might be much better ways to discover whether two elements could possibly be conjugates: for example by checking if the elements had different orders using gporder. isconjugate will allow you to process coset systems using the usual -cos subsuffix syntax, though the autohor is no sure why you would ever want to do this. In this case the two words will be considered to be conjugate if there is some word u such that u^-1*word*u and word2 are in the same coset.

If only one word is specified isconjugate will only stop if the word has finitely many conjugates, at which point it will output a list containing all of them.

isnormal [loglevel] groupname [subsuffix]


isnormal [loglevel] groupname [subsuffix]

Assuming automata or a similar program has computed an automaton that allows coset word-reduction to take place, isnormal will tell you whether the specified subgroup is normal. If is not, then it will list a subgroup generator and a group generator that shows this.

Programs provided for compatibility with KBMAG

automata includes all the functionality of KBMAG's separate autgroup, kbprog, gpmakefsa, gpaxioms, autcos (including gpsubwa and gpsubpres), and kbprogcos, and gpminkb and a little more besides. In general, a KBMAG command line that begins with any of these program names will work as a command line to MAF, with the program name changed to automata, and the output will include equivalents of all the files the KBMAG command would have generated. However, in some cases one or more extra command line options will be needed to stop automata from also producing other output that the original command would not have, or from doing work that would not have been necessary in KBMAG. Therefore versions of all these separate programs are provided in MAF, and in this case the same command line should produce equivalent results. However, unless you require strict compatibility with KBMAG, there will usually be no need to use any of them, once you are used to the slightly different way in which automata is used. So although MAF includes executable files with these names, they are all more or less identical to automata, and differ only in the default values given to a few of the options.

None of these programs has any facilities not provided in automata. They are provided solely with the aim of improving compatibility between MAF and KBMAG, and for the benefit of users who are familiar with it. They can all safely be deleted if you do not have any special requirements for compatibility between MAF and KBMAG.

Fuller descriptions of the KBMAG options accepted in the MAF version of KGBMAG's two key programs gpmakefsa and kbprog are given below.


gpmakefsa [loglevel] [format] [-cos] groupname subgroup_suffix

Construct the word-acceptor and general multiplier finite state automata for the shortlex automatic group or automatic coset system, of which the rewriting system defining the group is in the file groupname or the coset system is in groupname/cosname.


These options are ignored. MAF will make intelligent decisions about how to build the word acceptor and multiplier.

-me maxeqns

This option is ignored. In the KBMAG version of gpmakefsa it specifies an upper limit on the number of equations that are processed when correcting the difference machines during a failed correctness test. In MAF as many equations as can be found are processed, but the correctness test is aborted once it appears that all the new equations that are being discovered would all be recognised by the updated word difference machine.

-mwd maxwdiffs

This option is ignored. In the KBMAG version of gpmakefsa this puts an upper limit on the number of word-differences allowed after the correction. There is no good reason to have such an option.


kbprog [loglevel] [-ve] [-vwd] [-r | -ro | -resume] [-me n] [-mlr l r] [-mo n] [-hf h] rwsname

The KBMAG version of kbprog has zillions of options. Only those that are actually supported in the MAF version are listed above. In the detailed description that follows other KBMAG options that are accepted for compatibility purposes, but ignored, are also listed. In MAF kbprog is a version of automata that is modified so that it will only generate the automata that the KBMAG version of kbprog is capable of producing. This means that it will output either a confluent rewriting system, or word difference machines, or possibly both. However there are some differences in the output files:

The input file is shown as rwsname because kbprog accepts coset rewriting systems. In fact it also accepts the -cos option and the subsuffix, and in this case behaves identically to the MAF version of kbprogcos


In addition to the options listed here the MAF version of kbprog actually also accepts the options accepted by the automata program. But since you will normally only use this because you are emulating KBMAG, there is very little reason why you would use any options that were not in KBMAG.

-cn confnum

This option has no effect. In the KBMAG version of kbprog it controls how often the set of equations is tested for confluence. In MAF this option is not relevant because the algorithm which finds overlaps is a test for confluence. A sign that a system is about to become confluent is that MAF is suddenly able to process very large numbers of equations in a very short time.

-hf halting_factor

The KBMAG version of autgroup uses this to prevent kbprog from running for ever. Because MAF works in a very different way internally, it is not possible to give this option the same interpretation as in KBMAG. However, it has a somewhat similar effect. The lower the number passed as halting_factor, the more likely MAF is to decide that "enough" word differences have been found, and to terminate.

-me maxeqns

This puts a limit on the number of primary reductions that will be found. If exceeded the program will stop and output its current set of equations. By default there is no limit. It can also be set as the field maxeqns in the input file.

-mlr maxlenleft maxlenright

If this is used, then so far as possible only equations in which the left and right hand sides have lengths at most maxlenleft and maxlenright, respectively, are kept (MAF cannot always respect this option because it can cause inconsistencies in its internal data structures which it will not allow. In fact it is clear that even KBMAG does not always respect it, since on several of the examples where it is used several of the equations in the confluent system exceed the limits). With MAF, this option is not currently recommended. The author does not know of any input files in which using this option improves MAF's behaviour, and knows of several where it is counter-productive. If you have used the corresponding option in KBMAG and now want to process the same input file in MAF then first try to run without this option. Only try with this option if necessary. In the author's limited experience values that work with KBMAG are always too small in MAF. Values that are each twice what was used in KBMAG, or equal to the correct maximums as given by the confluent rewriting system, if known, whichever is the greater, may work.

This option can also be set as a field in the input file. The syntax for this is

maf_maxstoredlen := [maxlenleft,maxlenright]

-mo maxoverlaplen

The Knuth-Bendix algorithm works by forming a word which contains two overlapping reducible words, so that if the reductions are not yet consistent with one another two different reductions for the same word will arise, giving rise to a new equation. This option limits the maximum length of this "overlap" word, and once all possible overlaps up to this length have been considered MAF will bheave as though the rewriting system was confluent, even though it is not.

The only good reason for using this option in MAF, is when you know that MAF will not be able to find correct automata, and you are willing to accept provisional automata. Even quite a "short" word acceptor can usually eliminate most reducible words, so that a program that needs to enumerate group elements, and does not mind if occasionally the same element is enumerated twice, but would prefer to enumerate each element as few times as possible, can benefit from having such an acceptor available.

This parameter can also be set as the field maxoverlaplen in the input file.

-mrl maxreducelen

This option does nothing. In KBMAG it controls the maximum length a word can reach. In MAF the limit is 65533 (not 65535!) and this cannot be changed except by rebuilding MAF with a different value for the MAX_WORD constant, and a change in the definition of the Ordinal type. You are strongly recommended not to try to do this, as if a word ever reaches such an extraordinary length MAF will probably become extremely slow and encounter stack overflow errors. This limit is only likely to be exceeded if you are using a recursive ordering on words.

-ms maxstates

This option does nothing. In KBMAG it controls the maximum number of states in the reduction FSA.

-mt min_time]

This option roughtly like it does in KBMAG: unless confluence is achieved, MAF will not abort until at least the specified amount of time has elapsed since MAF began Knuth Bendix expansion.

-mwd maxworddiffs

This option is ignored, and is for KBMAG compatibility. There is no special reason in MAF to limit the number of word differences. However, if a group has more than around 4000-5000 word differences then it is highly unlikely to be automatic unless it turns out to be finite, and even in this case the multiplier may well be too large to compute, and the reduction FSA will be a better choice for doing word reduction.


This means resume after a previous run in which the output set of equations was not confluent. Input will be taken from monoidname.pkbprog or monoidname.kbprog (or both, if both exist) as well as monoidname. This may be useful if the program halted on a previous run due to some limit being exceeded, (or because you interrupted it) and you wish to resume with a higher limit. This option works differently from KBMAG, where the words as well as would be replaced by instead of.

-rk minlen mineqns

This option does nothing. In the KBMAG version of kbprog it enables the "Rabin-Karp" algorithm for word-reduction. In MAF very long equations are are not usually available for performing reductions. However, if word differences are being computed then unusually long words are reduced with the word difference machine.


In the MAF version of kbprog -ro is synonymous with -r. In the KBMAG version -ro works like the -r option does in MAF.

-sort maxoplen

This option does nothing. In the KBMAG version of kbprog it causes equations to be output in order of increasing length of their left hand sides. MAF always outputs equations in BFS order.

-t tidyint

This option does nothing. In the KBMAG version of kbprog it controls the frequency at which equations are tidied.

Unsupported options

This list is not guaranteed to be complete!


In the KBMAG version of kbprog these options change the word-ordering from the one specified in the input file. In the MAF version using these options will cause MAF to exit immediately with an error message.

Miscellaneous Programs

For full details of the programs listed below refer to the usage information that is displayed when you run them without any options.