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.