The following technical report is available from http://aib.informatik.rwth-aachen.de:
Static Termination Analysis for Prolog using Term Rewriting and SAT Solving Peter Schneider-Kamp AIB 2008-17
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 eneral, 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.