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.)
Download
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.
Usage
./mascott <file> <options> calls
mascott
on the given file. The input problem is assumed to be in
TPDB format
.
Possible options are the following:
General
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>.
Experiments