This site provides supporting material for the paper Normalized Completion Revisited by Sarah Winkler and Aart Middeldorp, submitted to CSL 2012. (Details on termination tools used in the setting of multi-completion can be found in this JAR submission on MKBtt which was accepted for publication.)


The tool mascott is available as a bytecode executable for Linux (32 bit), but you can also obtain the sources and compile the tool yourself. Some hints on how to call mascott are given below.


./mascott <file> <options> calls mascott on the given file. The input problem is assumed to be in TPDB format . Possible options are the following:
mascott performs normalized completion modulo some theory, represented as a convergent rewrite system. This representation can be supplied as input, specified with the flag -th <file>. This TRS is expected to be in TPDB format as well. If no such file is supplied, mascott detects an applicable theory automatically (currently ACU, groups and rings are supported besides AC). (Some example theories are contained in the archive of mascott sources). The global time limit is given by -t <seconds>. Further options are -st and -ct to output useful statistics and the completed system, respectively. -h displays the list of options.
Termination Checks
By default, termination checks are performed internally by TTT2, also specified by the option -it. The applied termination techniques can be controlled by -s <strategy> in the TTT2 strategy language. Alternatively, termination can be checked externally if an appropriate script is supplied using the option -tp <script>. The script is supposed to be executable from the current directory and it has to be compatible with the following minimal interface:
<script> <file> checks termination of the given system in TPDB format. It must print YES on the first line of standard output if termination could be established and something else otherwise. The time limit for each termination check is specified by -T <seconds>.