The Nagoya Termination Tool (NaTT)

Features

NaTT 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 . 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