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"
}