2022/07/12  Version 2.3: For competitions. 
2022/01/17  Version 2.1.1: Bugfix (thanks to Kiraku Shintani and Nao Hirokawa) 
2021/05/07  Version 2.1: New XMLbased interface and new multidimensional intepretations. 
2019/05/27  Version 1.9: Supported probabilistic rewriting. 
2019/02/14  Version 1.8: Release for a TACAS paper [SY19]. 
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 an XML format.
This section is under revision!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 RTA 2008, LNCS 5117, pp. 110–125, 2008. 
[GTS04]  The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs In LPAR 2004, LNAI 3452, pp. 75–90, 2004. 
[GTS05]  Proving and Disproving Termination of HigherOrder Functions In FroCoS 2005, LNAI 3717, pp. 216–231, 2005. 
[HM04a]  Dependency Pairs Revisited In RTA 2004, LNCS 3091, pp. 249–268, 2004. 
[HM04b]  Polynomial Interpretations with Negative Coefficients In AISC 2004, 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 RTA 2006, LNCS 4098, pp. 328–342, 2006. 
[INVY15]  Reducing Relative Termination to Dependency Pair Problems In CADE25, 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 LPAR 2007, LNAI 4790, pp. 348–362, 2007. 
[ST11]  Generalized and Formalized Uncurrying In FroCoS 2011, LNAI 6989, pp. 243–258, 2011. 
[SY19]  Reachability Analysis for Termination and Confluence of Rewriting In TACAS 2019, 2019. 
[WZM12]  Ordinals and KnuthBendix Orders In LPAR 2012, LNCS ARCoSS 7180, pp. 420–434, 2012. 
[YKS13a]  Unifying the KnuthBendix, Recursive Path and Polynomial Orders In PPDP 2013, pp. 181–192, 2013. 
[YKS13b]  Partial Status for KBO In WST 2013, pp. 74–78, 2013. 
[YKS14]  Nagoya Termination Tool In RTAiTLCA 2014, LNCS 8560, pp. 466–475, 2014. 
[YKS15]  A Unified Order for Termination Proving SCP, 111:110–134, 2015. 