This site provides supporting material for the paper Ordered Completion with Termination Tools by Sarah Winkler and Aart Middeldorp. Proofs omitted in the paper due to reasons of space can be found in the report version.

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.)