Applying static analysis techniques for inferring termination conditions of logic programs

We present the implementation of M, a system for universal left-termination inference of logic programs. Termination inference generalizes termination analysis/checking. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided to the system, requiring user annotations. With termination inference such annotations are no longer necessary. Instead, all provably terminating classes to all related predicates are inferred at once. The architecture of cTI is described(1) and some optimizations axe discussed. Running times for classical examples from the termination literature in LP and for some middle-sized logic programs are given.