mkbTT
This site provides supporting material for the paper Optimizing mkbTT by Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara. It contains information about version 2.0 of the tool mkbTT. To access the old version of this page on mkbTT 1.0, see here.

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.