Download
The tool oMKBtt is available as a bytecode executable for Linux. Some hints on how to call oMKBtt are given below.Usage
./omkbtt <file> <options>
calls oMKBtt 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.
-h
displays the list of options and -v <n>
controls the verbosity, where n
is a value between 0 and 3.
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>
.
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.
Experiments
To test oMKBtt for theorem proving purposes, problems in the TPTP 3.6.0 UEQ division were used. In the case of ordered completion, oMKBtt was run on the associated theories. Detailed results can be found here.Having a variety of termination strategies at its disposal, oMKBtt can e.g. find a ground complete system for this little problem, which can not be solved with standard orderings such as plain KBO or LPO. (oMKBtt uses a polynomial interpretation.)