Static Termination Analysis for Prolog using Term Rewriting and SAT
Solving
Peter Schneider-Kamp
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. Thus, termination
of logic programs is widely studied and significant advances have been
made during the last decades. Nowadays, there are fully-automated tools
that try to prove termination of a given logic program w.r.t. a given
class of inputs. Nevertheless, there still remain many logic programs
that cannot be handled by any current termination technique for logic
programs that is amenable to automation.
Another area where termination has been studied even more intensively is
term rewriting. This basic computation principle underlies the evaluation
mechanism of many programming languages. Significant advances towards
powerful automatable termination techniques during the last decade
have yielded a plethora of powerful tools for proving termination
automatically.
In this thesis, we show that techniques developed for proving termination
of term rewriting can successfully be adapted and applied to analyze
logic programs. The new techniques developed significantly extend the
applicability and the power of automated termination analysis for logic
programs. The work presented here ranges from adapting techniques to
work directly on logic programs to transformations from logic programs to
a specialized version of term rewriting. On the logic programming side
we also present a new pre-processing approach to handle logic programs
with cuts. On the term rewriting side we 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 developed in this thesis are implemented in tools
for automated termination analysis -- mostly 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 all years since 2004, where the leading automated tools
try to analyze termination of programs from different areas of computer
science.