The Nagoya Termination Tool (NaTT)

Features

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

News

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.

Downloads

NaTT Version 1.6 [OCaml code]

Third Party Libraries

NaTT is linked with ocamlgraph.

Documentation

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 the WST format.

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:

Contact

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

References

[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 Proc. 19th RTA, 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 Proc. 11th LPAR, LNAI 3452, pp. 75–90, 2004.
[GTS05] J. Giesl, R. Thiemann, P. Schneider-Kamp Proving and Disproving Termination of Higher-Order Functions In Proc. 5th FroCoS, LNAI 3717, pp. 216–231, 2005.
[HM04a] N. Hirokawa, A. Middeldorp Dependency Pairs Revisited In Proc. 15th RTA, LNCS 3091, pp. 249–268, 2004.
[HM04b] N. Hirokawa, A. Middeldorp Polynomial Interpretations with Negative Coefficients In Proc. 7th AISC, 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 Proc. 16th RTA, LNCS 4098, pp. 328–342, 2006.
[INVY15] J. Iborra, N. Nishida, G. Vidal, A. Yamada Reducing Relative Termination to Dependency Pair Problems In Proc. 25th CADE, 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 Proc. 14th LPAR, LNAI 4790, pp. 348–362, 2007.
[ST11] C. Sternagel, R. Thiemann Generalized and Formalized Uncurrying In Proc. 8th FroCoS, LNAI 6989, pp. 243–258, 2011.
[WZM12] S. Winkler, H. Zankl, A. Middeldorp Ordinals and Knuth-Bendix Orders In Proc. 18th LPAR, LNCS ARCoSS 7180, pp. 420–434, 2012.
[YKS13a] A. Yamada, K. Kusakari, T. Sakabe Unifying the Knuth-Bendix, Recursive Path and Polynomial Orders In Proc. 15th PPDP, pp. 181–192, 2013.
[YKS13b] A. Yamada, K. Kusakari, T. Sakabe Partial Status for KBO In Proc. 13th WST, pp. 74–78, 2013.
[YKS14] A. Yamada, K. Kusakari, T. Sakabe Nagoya Termination Tool In Proc. Joint 25th RTA and 12th TLCA, LNCS 8560, pp. 466–475, 2014.
[YKS15] A. Yamada, K. Kusakari, T. Sakabe A Unified Order for Termination Proving SCP, 111:110–134, 2015.