Static Termination Analysis for Prolog using Term Rewriting and SAT Solving

 

Jan Peter Schneider-Kamp

 

Abstract:

 

The most fundamental decision problem in computer science is the halting problem,
i.e., given a description of a program and an input, decide whether the program terminates
after finitely many steps or runs forever on that input. While Turing showed
this problem to be undecidable in general, developing static analysis techniques that
can automatically prove termination for many pairs of programs and inputs is of great
practical interest.

This is true in particular for logic programming, as the inherent lack of direction in the
computation virtually guarantees that any non-trivial program terminates only for certain
classes of inputs.

In this talk, we show that techniques developed for proving termination of term rewriting
can successfully be applied to analyze logic programs. The new techniques developed
significantly extend the applicability and the power of automated termination
analysis for logic programs.

In particular, we present a new pre-processing approach to transform logic programs
with cuts into cut-free logic programs. Then, a new transformations from logic programs
to a specialized version of term rewriting makes it possible to reuse techniques
developed for termination analysis of term rewriting. We also show how to
search for certain popular classes of well-founded orders on terms more efficiently by
encoding the search into satisfiability problems of propositional logic.
The contributions presented in this talk are implemented in our fully automated termination
prover AProVE. The significance of our results is demonstrated by the fact that
AProve has reached the highest score both for term rewriting and logic programming
at the annual international Termination Competitions in 2004, 2005, 2006, 2007, and
2008. In this competition, the leading automated tools try to analyze termination of
programs from different areas of computer science.