cTI: Bottom-Up Termination Inference for Logic Programs.
Serge Burckel, Sébastien Hoarau, Frédéric Mesnard, Ulrich Neumerkel · 2000
. We present cTI, a system for bottom-up termination inference. Termination inference is a generalization of 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 not necessary. Instead, all provably terminating classes to all related predicates are inferred at once. The architecture of cTI is discussed, highlighting several new aspects to termination analysis. The notion of termination neutral arguments is introduced, which helps to narrow down the actual arguments responsible for termination in a norm independent manner. We show how our approach can be adopted to realize an incremental system able to reuse previously inferred results, thereby allowing to use the system within a programming environment. Further we show how termination inference serves to tackle generalizations of th...