NTI

NTI (Non-Termination Inference) is a tool that can be used for automated non-termination proofs of term rewrite systems, string rewrite systems and logic programs.

What inputs are supported?

NTI accepts the input formats for Term/String Rewrite Systems (XML and old format) as specified in TPDB. It also accepts the input format for Logic Programs as specified in the termination portal.

What properties can be verified?

Termination and non-termination.

What external tools are used? (e.g., compilers, SMT solvers)

None.

What is the tool’s URL?

https://github.com/etiennepayet/nti

Example(s)

See the Termination Problem DataBase (TPDB).

References

• [Payet & Mesnard, TOPLAS'06]
• [Payet, TCS'08],
• [Payet, LOPSTR'18]
• [Payet, accepted in Journal of Automated Reasoning, December 2023]