NTI: Non-Termination Inference

NTI is a tool that can be used for automated non-termination proofs of term rewrite systems, string rewrite systems and logic programs. It implements the techniques described in the papers below. When a proof of non-termination is successfully performed, NTI provides an example of a non-terminating term, string or atomic query (depending on the paradigm). Only standard rewriting and pure logic programming are implemented for the moment.

Tool

Papers


Valid XHTML 1.0 Strict