The Nagoya Termination Tool (NaTT)

Features

• its power due to the implementation of the weighted path order (WPO) [YKS13a, YKS15],
• its efficiency due to the strong cooperation with external SMT solvers, and
• use of the DP framework for proving relative termination [INVY15].

News

Downloads

Third Party Libraries

Documentation

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

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:

• --smt "command": Uses the solver invoked by command for back-end. The solver should be configured to process SMT-LIB 2.0 scripts given through the standard input.
• --z3: Specifies Z3 version 4.0 or later for back-end. This option, choosen by default, is a shorthand for --smt "z3 -smt2 -in".
• --cvc4: Specifies CVC4 for backend. Equivalent to --smt "cvc4 --incremental --produce-models"

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

• EDG
  The estimated dependency graph processor [AG00, HM04a, GTS05].
• UNCURRY
  The uncurrying processor [HMZ13, ST11]. Currently, it can be applied only right before the EDG processor.
• LOOP
  A naive loop detection. Currenly, it can be applied only at the last.
• WPO [option]
  The weighted path order [YKS13a, YKS15] forms the core of NaTT. It is applied as a reduction pair processor if it is specified after 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:algebra
    Specifies a template algebra for weights in pol, max, or mpol. (default: pol)
  • -w[:neg]/-W
    Enable/disable weights. Negative constants are also allowed if :neg is specified (cf. [HM04b]). (default: enabled, non-negative)
  • -c[:n]/-C
    Enable/disable coefficients. If n is the character 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 back-end SMT solver must support QF-NIA logic. For rule removal processors, 1 is added to (top-left elements of) coefficients to maintain monotonicity.
  • --dim:n
    Uses the matrix interpretation of dimmension n for weights. Currently, this option cannot be combined with -a:max or -a:mpol options.
  • -s:{t/p/e}
    Use total / partial [YKS13b] / empty statuses.
  • -p[:s]/-P
    Enable/Disable (strict) precedences.
  • -f/-F
    Enable/Disable collapsing argument filters.
  • -Z
    Exclude 0 from the domain of the weight algebra (for KBO).
  • --adm
    Imposes the admissibility constraint (for KBO).

• The Knuth-Bendix order [KB70] (with argument filters [AG00]) is obtained as KBO, which is a shorthand for WPO -Z --adm.
• The transfinite KBO [LW07, WZM12] can be obtained as KBO -c[:n].
• The polynomial interpretation method [L75] is obtained as POLO, which is a shorthand for WPO -s:e -P -F.
• The matrix interpretation method [HW06, EWZ08] can be obtained as POLO --dim n, where n is the dimension.
• Certain forms of max-polynomial interpretations [FGMSTZ08] is obtained as POLO -a:mpol.
• The lexicographic path order [KL80] (with argument filters) is obtained as LPO, a shorthand for WPO -a:max -W.
• The recursive path order [D82] (with argument filters) is obtained as RPO, a shorthand for WPO -a:max -W --mset.

Contact

References