This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination prover for term rewrite systems. The main features of the tool are: the first implementation of the weighted path order which subsumes most of the existing reduction pairs, and the efficiency due to the strong cooperation with external SMT solvers. We present some new ideas that contribute to the efficiency and power of the tool. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Yamada, A., Kusakari, K., & Sakabe, T. (2014). Nagoya termination tool. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8560 LNCS, pp. 466–475). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_32
Mendeley helps you to discover research relevant for your work.