The Nagoya Termination Tool (NaTT)


NaTT [YKS14] is a termination prover for term rewrite systems (TRSs), which is special for:


2022/07/12Version 2.3: For competitions.
2022/01/17Version 2.1.1: Bugfix (thanks to Kiraku Shintani and Nao Hirokawa)
2021/05/07Version 2.1: New XML-based interface and new multi-dimensional intepretations.
2019/05/27Version 1.9: Supported probabilistic rewriting.
2019/02/14Version 1.8: Release for a TACAS paper [SY19].
2016/09/12Version 1.6: Competition version.
2016/04/21Version 1.5: Supported AC termination (certifiable, via experimental option -x).
2016/02/07Version 1.4: A bugfix for relative termination.
2015/07/02Version 1.3: Competition version.
2015/02/22Version 1.2: Supported relative termination.
2014/06/17Version 1.1 released.
2014/02/12Version 1.0 released.


NaTT Version 2.3 [OCaml code]

Third Party Libraries

NaTT is linked with ocamlgraph.


The command line of NaTT is in the following syntax:

./NaTT [file] [option]... [processor]...

The TRS whose termination should be verified is read from either the specified file or the standard input. The format should follow an XML format.

This section is under revision!

To execute NaTT, an SMT-LIB 2.0 compliant solver must be installed. The following options are provided for specifying such an SMT solver for back-end of NaTT:

NaTT is based on the dependency pair (DP) framework [AG00, HM04a, GTS04]. The following DP processors are available:

The following well-known reduction pairs are also supported, which are obtained as instances of WPO:


In case you find bugs, comments, or suggestions, please contact the author: Akihisa Yamada.


[AG00] T. Arts, J. Giesl Termination of Term Rewriting Using Dependency Pairs TCS, 236(1-2):133–178, 2000.
[D82] N. Dershowitz Orderings for term-rewriting systems TCS, 17(3):279–301, 1982.
[EWZ08] J. Endrullis, J. Waldmann, H. Zantema Matrix Interpretations for Proving Termination of Term Rewriting JAR, 40(2-3):195–220, 2008.
[FGMSTZ08] C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-Kamp, R. Thiemann, H. Zankl Maximal Termination In RTA 2008, LNCS 5117, pp. 110–125, 2008.
[GTS04] J. Giesl, R. Thiemann, P. Schneider-Kamp The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs In LPAR 2004, LNAI 3452, pp. 75–90, 2004.
[GTS05] J. Giesl, R. Thiemann, P. Schneider-Kamp Proving and Disproving Termination of Higher-Order Functions In FroCoS 2005, LNAI 3717, pp. 216–231, 2005.
[HM04a] N. Hirokawa, A. Middeldorp Dependency Pairs Revisited In RTA 2004, LNCS 3091, pp. 249–268, 2004.
[HM04b] N. Hirokawa, A. Middeldorp Polynomial Interpretations with Negative Coefficients In AISC 2004, LNAI 3249, pp. 185–198, 2004.
[HMZ13] N. Hirokawa, A. Middeldorp, H. Zankl Uncurrying for Termination and Complexity JAR, 50(3):279–315, 2013.
[HW06] D. Hofbauer, J. Waldmann Termination of String Rewriting with Matrix Interpretations In RTA 2006, LNCS 4098, pp. 328–342, 2006.
[INVY15] J. Iborra, N. Nishida, G. Vidal, A. Yamada Reducing Relative Termination to Dependency Pair Problems In CADE-25, LNCS 9195, pp. 163–178, 2015.
[KB70] D.E. Knuth, P. Bendix Simple Word Problems in Universal Algebras In Computational Problems in Abstract Algebra, pp. 263–297, Pergamon Press, 1970.
[KL80] S. Kamin, J.-J. Lévy Two generalizations of the recursive path ordering Unpublished note, Dept. of Comuter Science, Univ. of Illinois, 1980.
[L75] D. Lankford Canonical algebraic simplification in computational logic Technical Report ATP-25, University of Texas, 1975.
[LW07] M. Ludwig, U. Waldmann An Extension of the Knuth-Bendix Ordering with LPO-Like Properties In LPAR 2007, LNAI 4790, pp. 348–362, 2007.
[ST11] C. Sternagel, R. Thiemann Generalized and Formalized Uncurrying In FroCoS 2011, LNAI 6989, pp. 243–258, 2011.
[SY19] C. Sternagel, A. Yamada Reachability Analysis for Termination and Confluence of Rewriting In TACAS 2019, 2019.
[WZM12] S. Winkler, H. Zankl, A. Middeldorp Ordinals and Knuth-Bendix Orders In LPAR 2012, LNCS ARCoSS 7180, pp. 420–434, 2012.
[YKS13a] A. Yamada, K. Kusakari, T. Sakabe Unifying the Knuth-Bendix, Recursive Path and Polynomial Orders In PPDP 2013, pp. 181–192, 2013.
[YKS13b] A. Yamada, K. Kusakari, T. Sakabe Partial Status for KBO In WST 2013, pp. 74–78, 2013.
[YKS14] A. Yamada, K. Kusakari, T. Sakabe Nagoya Termination Tool In RTAi-TLCA 2014, LNCS 8560, pp. 466–475, 2014.
[YKS15] A. Yamada, K. Kusakari, T. Sakabe A Unified Order for Termination Proving SCP, 111:110–134, 2015.