Usage
The following paragraphs describe the command-line interface of mkbTT. The call$ ./mkbtt <file> <options>
- the trs format used in TPDB up to version 5.*,
- the newer xml format used in TPDB from version 7.* onwards, and
- the TPTP3 format.
General
The global time limit is given by -t <seconds> .
To control the output, use -st, -ct and
-p to obtain some statistics, the completed system, and a proof
of the saturation, 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 <file>, a rewrite system can be supplied to check
whether it is complete and joins the input equalities.
The settings for the required termination check have to be specified as
described below.
Certification
mkbTT can output XML proofs in CPF which can be certified by CeTA. To this end, the script callcertify needs to be modified to output a certifiable termination proof. To obtain a certifiable completion proof, one can call mkbTT with option-cert as follows:$ ./mkbtt input/kb/slothrop_equiv_proofs_or.trs -cert > proof.xml
$ ceta proof.xml
In ordered completion mode, mkbTT can produce certifiable entailment
(dis)proofs using -cert and -p format ,
where format is one of
cpfconv (for conversions), cpfsub (for subsumption proofs with history),
or cpftree (for equational proof trees):$ ./mkbtt -o -cert -p cpfsub input/easy/GRP022-2.tptp > proof.xml$ ceta proof.xmlThe format of disproofs is ndependent of the choice of <format>, e.g. in
$ ./mkbtt -o -cert -p cpfsub input/easy/BOO027-1.tptp > proof.xml$ ceta proof.xmlmkbTT has also some very basic theorem proving feature in normalized completion mode. For instance, CeTA certifies the following entailment proof:
$ ./mkbtt -n -cert -p cpfsub input/certification/groups0.tptp -s acrpo > proof.xml$ ceta proof.xmlPlease note that certification of entailment proofs requires CeTA ≥ 2.18.
Termination checks
By default, termination checks are performed internally using TTT2. 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> <timeout> is supposed to check
termination of the given system in TPDB format and print YES on the first
line of standard output if termination could be established. The parameter
<timeout> specifies a time limit in seconds for a termination
check (if it is ignored mkbTT just kills the process).
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, slothrop
and sum. The max strategy is used by default.
Term indexing
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, the latter is applied by default.
Besides, the option -ui <technique> allows to select an
indexing technique for the retrieval of unifiable terms in deduce steps.
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.
Isomorphisms
The option -is <iso> is used to control process isomorphisms,
where <iso> may take the values rename or
rename+ to incorporate checking for renamings,
perm or perm+ to check for argument permutations,
none to suppress isomorphism checks or auto to
heuristically choose a possibly applicable isomorphism at the beginning
of a run (the latter is used by default). A trailing +
indicates that checks are repeatedly performed in every iteration, and not
just when a process is split.