\section{Logic Programming}\label{subsec:lp}

In this category, the tools have to prove termination of \textsf{Prolog}
programs for given sets of queries. 
Although there exist many tools
for  proving (and even disproving)
termination of logic programs,  only two tools joined
the competition 2008. In the future, we should try to improve this and
motivate the authors of the many other tools to participate as well.

Essentially, there are two approaches to prove termination of logic programs.
Either one proves termination directly on the basis of the logic program
or one transforms the logic program into a term rewrite system and proves
termination of the TRS afterwards. In the competition, the tool {\sf Polytool}
used the direct approach and the tool
{\sf AProVE}
used the transformational approach. The main feature of {\sf Polytool} is that
it contains several termination techniques that originate from term rewriting,
but which were adapted to logic programs. The main feature of {\sf AProVE} is
that it can handle arbitrary logic programs via transformation (not just
``well-moded'' logic programs as in earlier transformational tools). 
Both {\sf
Polytool} and {\sf AProVE} use SAT-solving  when searching for suitable orders
(in fact, {\sf Polytool} uses {\sf 
AProVE} as a back-end for this search).

In the competition, {\sf AProVE} was a little more powerful than {\sf
Polytool} ({\sf AProVE} could prove termination of 246 examples and {\sf
Polytool} proved termination for 238 examples out of 349).
This is most likely due to the fact that {\sf AProVE} offers more termination
techniques than {\sf Polytool}. But of course, these termination techniques
might also
adapted be to logic programming and integrated into {\sf Polytool} in the
future.



