TNT: A Transformation for analyzing Narrowing Termination
Click here for a short description of the technique...
TNT is a tool developed by Germán Vidal and Naoki Nishida to analyze the termination of narrowing. It takes a term-rewriting system (TRS) and a sequence of abstract terms that specify which arguments are ground for some user-defined functions; for instance, the abstract term append(g,v) specifies that the first argument of function append is ground and the second one is possibly a variable. This is similar to the notion of "modes" in logic programming. The transformation then proceeds basically as follows: Therefore, once the (possibly) non-ground arguments are filtered away, the termination of the transformed program can be analyzed with any termination prover for TRSs, like AProVE

A more detailed account of the technique can be found in this paper

Click here to close this window.

You can either write down the initial TRS or choose one from (a small selection of) the termination problem database (and then edit it). TRSs should basically follow the syntax of TRS input files (with some restrictions, e.g., the specification of a "strategy" is not allowed).

Once the TRS is loaded in, you can provide an abstract call (e.g., a call of the form app(g,v) in TRS tpdb-4.0/TRS/AG01/#3.12.trs or take(g,g,v) in TRS tpdb-4.0/TRS/SchneiderKamp/trs/otto02.trs, etc) and press the "Filter TRS" button to get the transformed TRS.

Initial TRSTransformed TRS
Choose a file: Abstract call:
labeling? deletion of non-reachable rules? (select only one checkbox!)
Now you can use any termination prover for TRSs in order to analyze the termination of the transformed TRS (e.g., AProVE).
Or you can simply click to check the termination of the transformed TRS using the web interface of the AProVE termination prover (using a fixed timeout of 60 secs).

Contact me at gvidal at dsic.upv.es if you want the source code.

*** Only tested in Chrome/Firefox ***

Last update / Germán Vidal