Abstract

We describe the Tyrolean Termination Tool, the successor of the Tsukuba Termination Tool, a powerful tool for automatically proving termination of rewrite systems based on the dependency pair method of Arts and Giesl. It incorporates several new techniques that make the method more efficient. The tool produces high-quality output and has a convenient web interface. We describe the differences between the two and explain the new features in some detail.

BibTeX

@inproceedings{HM-RTA05,
  author      = "Nao Hirokawa and Aart Middeldorp",
  title       = "Tyrolean Termination Tool",
  booktitle   = "Proceedings of the 16th International Conference on
                 Rewriting Techniques and Applications",
  series      = "Lecture Notes in Computer Science",
  volume      = 3467,
  pages       = "175--184",
  publisher   = "Springer-Verlag",
  year        = 2005
}