T y r o l e a n   T e r m i n a t i o n   T o o l


The Tyrolean Termination Tool is a tool for automatically proving termination of rewrite systems based on the dependency pair method of Arts and Giesl. It is described in the following paper by Nao Hirokawa and Aart Middeldorp:

The proof techniques used in the tool are described in the following papers (by the same authors): The Tyrolean Termination Tool is the successor of the award-winning Tsukuba Termination Tool, which is described in the following paper: The Tyrolean Termination Tool is not only much faster and more powerful than its predecessor, it also is has a more convenient user interface. Furthermore, in addition to ordinary first-order rewrite systems, it can handle simply-typed applicative rewrite systems. Such systems are transformed into ordinary first-order rewrite systems by the transformation described in the following paper: