Download
Besides the web interface, mkbTT is available as a bytecode executable for Linux. Some hints on how to call mkbTT are given below. Alternatively, you can retrieve the sources of a newer version.You might also want to download the systems used for experiments as a .tar.gz archive.
Usage
The following paragraphs describe the command-line interface of mkbTT. The call ./mkbtt <file> <options> invokes mkbTT
on the given file. The input problem must be either in
TPDB
or TPTP3 format.
Possible options are the following:
General
The global time limit is given by -t <seconds> .
Further options are -st and -ct to output
useful statistics and the completed system, respectively.
The flag
-h displays the list of possible options and
-v <n>
controls the verbosity, where n is a value between 0 and 3.
Using -ch, a rewrite system can be supplied to check
whether it completes the theory. The settings for the required termination
check have to be specified as described below.
Termination checks
By default, termination checks are performed internally using TTT2, also specified by the option -it. The applied termination
techniques can be controlled by using -s <strategy> and
specifying a strategy in the TTT2 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.
Here are examples for such scripts calling
AProVe
and μterm.
With both internal and external termination, the time limit for each termination check is specified by
-T <seconds> .
Node selection
To control the selection of nodes, the option -ss <strategy>
allows to supply a selection strategy in mkbTT's strategy
language. Predefined strategies are max, mkbtt1,
slothrop and sum.
Indexing techniques
The term indexing technique used for variant and encompassment retrievals in rewrite inferences can be specified via -ix <technique>, where nv denotes naive indexing, pi
denotes path indexing, dt specifies discrimination trees and
ct abbreviates code trees.
Critical pair criteria
By adding the flag -cp <cpc> a critical pair criterion
can be selected, where cpc can be
none or have one of the values prime,
blocked, connected or all denoting
the criteria PCP, BCP, CCP and all as outlined
in the paper. In addition, the option primeblocked combines
PCP with BCP such that all equations which are superfluous
according to one of these criteria get filtered out.
Isomorphisms
The options -is rename and
-is perm can be set to incorporate checking for renamings and
argument permutations, respectively. These checks are performed before a
process gets split. By adding a + the respective type of
isomorphism is checked for repeatedly in every iteration.
Experiments
The complete tables corresponding to the experiments presented in the paper can be found here.mkbTT can also complete the problem CGE4 which has not been achieved automatically before.