2016/09/12  Version 1.6: Competition version. 
2016/04/21  Version 1.5: Supported AC termination
(certifiable, via experimental option x ).

2016/02/07  Version 1.4: A bugfix for relative termination. 
2015/07/02  Version 1.3: Competition version. 
2015/02/22  Version 1.2: Supported relative termination. 
2014/06/17  Version 1.1 released. 
2014/02/12  Version 1.0 released. 
./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 SMTLIB 2.0 compliant solver must be installed. The following options are provided for specifying such an SMT solver for backend of NaTT:
smt "command"
:
Uses the solver invoked by command for backend.
The solver should be configured to process SMTLIB 2.0 scripts given
through the standard input.
z3
:
Specifies Z3 version 4.0 or later
for backend.
This option, choosen by default,
is a shorthand for smt "z3 smt2 in"
.
cvc4
:
Specifies CVC4 for backend.
Equivalent to smt "cvc4 incremental producemodels"
NaTT is based on the dependency pair (DP) framework [AG00, HM04a, GTS04]. The following DP processors are available:
EDG
UNCURRY
EDG
processor.
LOOP
WPO [option]
EDG
, and as
a rule removal processor [GTS04] otherwise.
For the latter case,
a care must be taken not to break monotonicity when choosing options.
Following options are available:
a:
algebrapol
,
max
, or
mpol
. (default: pol
)
w[:neg]/W
:neg
is specified
(cf. [HM04b]).
(default: enabled, nonnegative)
c[:n]/C
b
or t
,
then coefficients are in {0,1} or {0,1,2}, resp. and encoded in linear formulas.
If n is a number or omitted, then coefficients are
natural numbers (below n) and encoded in nonlinear formulas.
For the latter case, the backend SMT solver must support QFNIA logic.
For rule removal processors, 1 is added to (topleft elements of) coefficients
to maintain monotonicity.
dim:n
a:max
or a:mpol
options.
s:{t/p/e}
p[:s]/P
f/F
Z
adm
KBO
,
which is a shorthand for WPO Z adm
.
KBO c[:n]
.
POLO
, which is a shorthand for WPO s:e P F
.
POLO dim n
,
where n is the dimension.
POLO a:mpol
.
LPO
, a shorthand for WPO a:max W
.
RPO
, a shorthand for WPO a:max W mset
.
[AG00]  Termination of Term Rewriting Using Dependency Pairs TCS, 236(12):133–178, 2000. 
[D82]  Orderings for termrewriting systems TCS, 17(3):279–301, 1982. 
[EWZ08]  Matrix Interpretations for Proving Termination of Term Rewriting JAR, 40(23):195–220, 2008. 
[FGMSTZ08]  Maximal Termination In Proc. 19th RTA, LNCS 5117, pp. 110–125, 2008. 
[GTS04]  The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs In Proc. 11th LPAR, LNAI 3452, pp. 75–90, 2004. 
[GTS05]  Proving and Disproving Termination of HigherOrder Functions In Proc. 5th FroCoS, LNAI 3717, pp. 216–231, 2005. 
[HM04a]  Dependency Pairs Revisited In Proc. 15th RTA, LNCS 3091, pp. 249–268, 2004. 
[HM04b]  Polynomial Interpretations with Negative Coefficients In Proc. 7th AISC, LNAI 3249, pp. 185–198, 2004. 
[HMZ13]  Uncurrying for Termination and Complexity JAR, 50(3):279–315, 2013. 
[HW06]  Termination of String Rewriting with Matrix Interpretations In Proc. 16th RTA, LNCS 4098, pp. 328–342, 2006. 
[INVY15]  Reducing Relative Termination to Dependency Pair Problems In Proc. 25th CADE, LNCS 9195, pp. 163–178, 2015. 
[KB70]  Simple Word Problems in Universal Algebras In Computational Problems in Abstract Algebra, pp. 263–297, Pergamon Press, 1970. 
[KL80]  Two generalizations of the recursive path ordering Unpublished note, Dept. of Comuter Science, Univ. of Illinois, 1980. 
[L75]  Canonical algebraic simplification in computational logic Technical Report ATP25, University of Texas, 1975. 
[LW07]  An Extension of the KnuthBendix Ordering with LPOLike Properties In Proc. 14th LPAR, LNAI 4790, pp. 348–362, 2007. 
[ST11]  Generalized and Formalized Uncurrying In Proc. 8th FroCoS, LNAI 6989, pp. 243–258, 2011. 
[WZM12]  Ordinals and KnuthBendix Orders In Proc. 18th LPAR, LNCS ARCoSS 7180, pp. 420–434, 2012. 
[YKS13a]  Unifying the KnuthBendix, Recursive Path and Polynomial Orders In Proc. 15th PPDP, pp. 181–192, 2013. 
[YKS13b]  Partial Status for KBO In Proc. 13th WST, pp. 74–78, 2013. 
[YKS14]  Nagoya Termination Tool In Proc. Joint 25th RTA and 12th TLCA, LNCS 8560, pp. 466–475, 2014. 
[YKS15]  A Unified Order for Termination Proving SCP, 111:110–134, 2015. 