mkbTT
This site provides supporting material for the paper Multi-Completion with Termination Tools by Haruhiko Sato, Sarah Winkler, Masahito Kurihara and Aart Middeldorp.

Download

MKBtt is available as a bytecode executable for Linux. Some hints on how to call MKBtt are given below. To obtain the results listed in the table below, we used the script ttt2fast to interface a special version of TTT2 as a termination prover.
You might also want to download the systems used for experiments as a .tar.gz archive.

Usage

./mkbtt -tp <script> <file> calls MKBtt using the given script to check termination. The input file must be in TPDB format. Time limits are given as -t <seconds> for the overall time and -T <seconds> for the time per termination call. Further options are -st and -ct to output useful statistics and the completed system, respectively.

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.

Experiments

The following table is an extension of Table 4 in the paper. We present some experimental data obtained on a workstation equipped with an Intel Pentium M processor running at a CPU rate of 2 GHz on 1 GB of system memory and with a time limit of 1 hour. Column (1) shows the total time in seconds, column (2) the percentage spent on termination, column (3) the number of calls to the external termination prover, and column (4) the number of inference steps.

Experiments were performed using AProVE 07 with a 5 seconds time limit per termination call and TTT2 with a 1 second time limit, the latter with a restricted strategy which uses dependency pairs and the recursive SCC algorithm together with the subterm criterion and some simple strategies like counting function symbols, LPO and linear polynomials. For the last four columns, TTT2 libraries were included in MKBtt to check termination internally, using the same strategy as described above.


AProVE 07 TTT2fast
(termination checked externally) (termination checked externally) (termination checked internally)
Slothrop MKBtt Slothrop MKBtt MKBtt
system (1) (2) (3) (1) (2) (3) (4) (1) (2) (3) (1) (2) (3) (4) (1) (2) (3) (4)
SK90_3.01 800.37 97 326 85.30 99 51 29 71.52 67 304 4.45 79 51 29 1.18 22 51 29
SK90_3.03 163.51 98 86 90.97 98 53 29 9.97 65 86 6.19 63 53 29 2.71 16 53 29
SK90_3.04 508.24 55 658 140 954.90 57 1071 252
SK90_3.05 913.77 98 225 94 78.48 32 258 46.45 43 220 92 31.22 17 220 92
SK90_3.06 44.22 74 290 75 25.97 56 290 75
SK90_3.07 513.27 99 242 67 46.03 68 282 77 27.71 47 282 77
SK90_3.08 17.46 99 13 10.95 99 8 12 1.45 99 13 0.82 93 8 12 0.08 5 8 12
SK90_3.19 84.25 99 43 112.65 99 65 11 3.39 90 43 5.01 96 65 11 0.79 79 65 11
SK90_3.22 617.33 33 1406 141 557.79 26 1406 141
SK90_3.27 73.61 95 70 118.56 65 143 37 94.99 56 166 50
(a) 105.17 99 47 14 36.94 91 248 6.06 78 47 14 2.83 55 47 14
(b) 13.17 86 11 35.58 78 173 35 27.58 72 173 35
(c) 2793.21 99 1220 77 665.29 36 1384 246.64 85 1072 77 175.47 83 1072 77
(d) 201.84 96 105 233.19 99 133 45 22.25 47 105 13.97 80 133 45 5.04 47 133 45
(e) 248.95 99 99 15 78.64 82 608 33.65 83 305 33 12.34 74 271 20
(f) 13.39 99 8 14.40 99 9 7
SL_ackermann 12.08 99 8 13.26 99 10 5 0.24 96 8 0.33 91 10 5 0.02 50 10 5
SL_cge2 2793.21 99 1220 77 665.29 36 1384 246.64 85 1072 77 175.47 83 1072 77
SL_cge3
SL_endo 246.56 95 101 218.96 99 135 45 12.64 39 105 7.87 74 135 45 1.91 35 133 45
SL_equiv_proofs_or 53.47 82 262 230.35 92 1101 26 6.60 72 161 34
SL_equiv_proofs 54.47 82 266 230.06 92 1101 26 6.64 72 161 34
SL_fgh 5.19 99 3 7.06 99 3 4 0.10 90 3 0.10 90 3 4 0.00 ? 3 4
SL_groups_conj 51.97 99 34 51.19 99 27 14 1.48 71 34 1.03 83 27 14 0.15 33 27 14
SL_groups 46.71 97 30 96.94 99 49 35 2.10 46 30 2.28 71 49 35 0.59 19 49 35
SL_hard 7.08 99 3 6.38 99 3 3 0.10 99 3 0.09 99 3 3 0.00 ? 3 3
SL_nlp-2b
successes 12 18 20 23 23
total time 41250.41 40708.83 27044.60 13251.95 12911.98

The SK systems stem from J. Steinbach, U. Kühler, Check Your Ordering – Termination Proofs and Open Problems, Technical Report SR-90-25, Universität Kaiserslautern, 1990. Systems (a), (b), (e) and (f) are secret2006/torpa/secr4.srs, secret2006/torpa/secr10.srs, Zantema/z115.srs and SchneiderKamp/trs/thiemann27.trs from the termination competition web site. System (c) is CGE2 and system (d) is GE1, both taken from reference [8]. Systems with prefix SL come with the Slothrop code.

MKBtt can also complete CGE3 (described in reference [6]) which has not been achieved automatically before. Using TTT2micro (a variation of TTT2fast without polynomials), a result is obtained after 1.7 hours. The resulting TRS is a variation of the system described in reference [6] (it differs in that associativity is oriented in the other direction).

Moreover, our tool manages to complete this proof reduction system described in: I. Wehrman, A. Stump: Mining Propositional Simplification Proofs for Small Validating Clauses. ENTCS 144(2), pp. 79 - 91, 2006, yielding this result.