`app(A,B,C) terminates_if b(A);b(C)`

is
inferred for program `app/3`

. Here, `b(A)`

is true if the term size of `A`

is bound, e.g. finite and
ground. Disjunctions are denoted as `;`

. Thus,
`app/3`

has been proven to terminate, if the first or the
last argument is bound.
Termination inference is an *annotation free* generalization
of termination analysis/checking. It shifts the programmer's focus
away from particular cases to the whole relation. Traditionally, a
termination analyzer tries to prove that a given class of queries
terminates. This class must be provided by the user, which is rather
cumbersome if the programs have been written previously without any
annotations. With termination inference no annotations are necessary.
All provably terminating classes to all related predicates are
*inferred* at once, illustrating the `multi-directionality' of
predicates. This means that predicates can be used safely in several
`directions'.

- Analysis of existing programs (without any annotations).
- Analysis of classes of programs. Instead of a single program, a
set of related programs can be analyzed at once. Current uses:
- Determination of a static goal ordering to ensure termination [HoaMes98]. Here, an appropriate goal ordering is chosen out of the set of permutations.
- Determination of terminating program fragments used to aid a slicing-system in explaining reasons of nontermination. Terminating slices are eliminated out of the set of all failure-slices of a program [NeuMes99].

- Incremental analysis. Due to the bottom up nature of termination inference, predicates can be analyzed prior to the actual use in a program. This is in particular useful for libraries and incremental program development. In both cases, an incremental analysis avoids to go over unchanged parts again and again. Analysis time can therefore be significantly reduced.

cTI_lt has been integrated into GUPU, a Prolog programming environment for beginners used at TU Wien and Univ. de La Réunion. cTI_lt explains compactly the (provable) properties of termination of all predicates and improves a slicing-system in explaining reasons of nontermination.

- som4
- a rather complex termination condition
- exp
- a simple grammar with a very large cycle, same grammar as DCG
- reach
- example 7.6.2c from L.Plümer, Termination Proofs for Logic Programs, LNAI 446, 1990.
- APPEND3, NAIVE REVERSE, PERMUTATION
- from K.R.Apt, From Logic Programming to Prolog, Prentice-Hall, 1997.
- Benchmark collection
- including collection of Naomi Lindenstrauss

To determine the corresponding models, cTI uses heavily abstract interpretations. The current implementation uses SICStus Prolog relying most notably on its libraries CLP(Q) (to perform calculations in N) and CLP(B). For further details, please refer to the literature.

- Fred Mesnard
- idea, design, most implementation, maintenance
- Ulrich Neumerkel
- TNA, web interface, NTI
- Serge Colin
- implementation of mu-calculus
- Antoine Rauzy
- help and advice for boolean parts (mu-calculus)
- Sébastien Hoarau
- uses termination inference for static goal reordering
- Alexander Forst-Rakoczy
- human guide to HTML and Apache

[Mes96] F. Mesnard, Inferring left-terminating classes of queries for constraint logic programs. JICSLP'96, 7-21, MIT Press, 1996.

[HoaMes98] S. Hoarau and F. Mesnard, Inferring and Compiling Termination for Constraint Logic Programs. LOPSTR 1998, 240-254, LNCS 1559, Springer-Verlag, 1999.

[NeuMes99] U. Neumerkel and F. Mesnard, Localizing and explaining reasons for nonterminating logic programs with failure slices. PPDP'99, 328-341, LNCS 1702, Springer-Verlag, 1999.

[MesNeu01] F. Mesnard and U. Neumerkel, Applying static analysis techniques for inferring termination conditions of logic programs. SAS'01, 93-110, LNCS 2126, Springer-Verlag, 2001.

[MesPayNeu02] F. Mesnard, E. Payet, and U. Neumerkel, Detecting Optimal Termination Conditions of Logic Programs. SAS'02, 509-525, LNCS 2477, Springer-Verlag 2002.

TermiLog (without frames). Termination analyzer by Naomi Lindenstrauss.

TerminWeb. Termination analyser by Michael Codish and Cohavit Taboch.

TALP. Automatic termination proofs for well-moded logic programs.

LPTP. Logic program theorem prover (proving left termination and other properties) by Robert Stärk.

Ciao. Prolog development system with an upper-bound complexity analyzer. If the property steps_ub/2 with a finite upper-bound has been proven, also termination has been proven. Upper-bound analysis therefore generalizes termination analysis in another direction.

Mercury contains a termination analyser (Manual).

Hasta-La-Vista. Termination analyser for logic programs equipped with numerical computations.

Fred Mesnard (Université de La Réunion), Ulrich Neumerkel (Technische Universität Wien)