Tsukuba Termination Tool
Nao Hirokawa and Aart Middeldorp
Proceedings of the 14th International Conference on Rewriting Techniques
and Applications (RTA 2003), Lecture Notes in Computer Science 2706,
pp. 311 – 320, 2003
Abstract
We present a tool for automatically proving termination of first-order rewrite systems. The tool is based on the dependency pair method of Arts and Giesl. It incorporates several new ideas that make the method more efficient. The tool produces high-quality output and has a convenient web interface.BibTeX Entry
@inproceedings{HM-RTA03,
author = "Nao Hirokawa and Aart Middeldorp",
title = "Tsukuba Termination Tool",
booktitle = "Proceedings of the 14th International Conference on Rewriting
Techniques and Applications",
series = "Lecture Notes in Computer Science",
volume = 2706,
pages = "311--320",
year = 2003,
doi = "10.1007/3-540-44881-0\_22"
}
© Springer
René Thiemann noticed a serious bug in the implementation of KBO, which affects columns (4), (5), and KBO in Table 2. The new data is given below. Consequently, the claim in Section 5 that the termination of Example 33 (Battle of Hydra and Hercules) in [6] can be proved by TTT has to be retracted. (The bug has been corrected in the meantime.)
The data in column (6) is obtained with all argument filterings
and the other options the same as for columns (4) and (5).
(4) |
(5) |
KBO | (6) |
||
| [3, Example 3.3] | 129.57 |
? |
0.00 |
? |
|
| [3, Example 3.4] | 1.12 |
16.80 |
0.00 |
0.72 |
|
| [3, Example 3.9] | 398.94 |
? |
0.00 |
6.66 |
|
| [3, Example 3.11] | 2.25 |
33.92 |
0.00 |
? |
|
| [3, Example 3.15] | 0.38 |
0.39 |
0.06 |
0.38 |
|
| [3, Example 3.38] | 0.02 |
7.73 |
0.00 |
1.01 |
|
| [3, Example 3.44] | 0.84 |
3.53 |
0.10 |
0.34 |
|
| [4, Example 6] | 0.08 |
280.04 |
0.00 |
8.81 |
|
| [6, Example 11] | 0.39 |
5.63 |
0.00 |
46.74 |
|
| [6, Example 33] | 0.20 |
31.21 |
0.00 |
17.98 |
|
| [15, Example 17] | 22.23 |
? |
0.00 |
? |
|
| [16, Example 4.27] | 2.40 |
8.29 |
0.16 |
239.21 |
|
| [16, Example 4.60] | 0.33 |
102.50 |
0.00 |
587.39 |
|
| [17, Example 58] | 0.48 |
0.47 |
0.07 |
0.05 |