\section{Term Rewriting}\label{subsec:trs}

In these categories, the
tools try to prove or disprove termination of term rewrite systems.
Unfortunately, this year several of the well-known tools in the area
did not participate. In the future, one should try to motivate their authors
to join this category again. Moreover, one should also encourage the tools to
join as many of the different TRS-sub-categories as possible.

\subsection{Full Termination of Term Rewriting}

In the category ``\emph{TRS Standard}'', one regards ordinary TRSs. 
Here, three tools participated on 1391 examples. The winner was {\sf AProVE}
which could prove termination for 995 TRSs and disprove termination for 231
examples. The second best tool was \TTTT\ which proved termination for 792
examples and disproved it for 178 TRSs. Finally, {\sf Jambox} proved
termination of 750 examples and disproved it for 60 TRSs.
New techniques employed by the tools in this competition include
polynomial interpretations that also allow functions like ``maximum'' and
``minimum'' as well as rational polynomial interpretations (where the search
for the interpretations is based on SAT-solving).

It is remarkable that \TTTT\ was using at most 5 seconds per problem,
and its total time (for YES answers) is an eighth of the winner's.
The authors wanted to show that even with severely limited resources,
a considerable score could be achieved.



\subsection{Innermost Termination of Term Rewriting}

The categories ``\emph{TRS Innermost}'' and ``\emph{TRS Outermost}''
regard term rewriting under the innermost resp.\ the outermost evaluation strategy. In the
innermost category, only {\sf AProVE} participated (proving
innermost termination of 241 examples and disproving it for 4 examples out of
358). Here, due to new techniques developed for disproving innermost
termination,
it would be interesting in the future to try to also disprove
innermost termination for the other TRS-examples that are known to be
non-terminating for full rewriting. 


\subsection{Outermost Termination of Term Rewriting}


In the outermost category, a competition took place a month later than the
rest of the competition. Here, several new results had been developed.
 In this category, \textsf{JamboxGoesOut} was the winner for proving
termination
 due to its
new transformation from outermost to context-sensitive rewriting. It proved
outermost termination for  72 out of 291 examples (but it did not disprove
outermost termination for any example). Concerning disproving
outermost termination, \TTTT was the winner
due to its new method to decide whether a loop is also an outermost loop.
It disproved outermost termination for 158
examples
(but it did not prove outermost termination for any example). The remaining two participants
were {\sf TrafO} (which proved 46 and disproved 30 examples) and {\sf AProVE}
(which proved 27 and disproved 37 examples).
{\sf TrafO} transforms  outermost termination problems
to standard termination problems
and then calls {\sf Jambox} or {\sf AProVE} to solve them.

\subsection{Termination Modulo Theory}

Here, one proves termination modulo AC. Unfortunately, only {\sf AProVE}
participated and proved termination for 57 and disproved it for 2 out of
71 examples.


\subsection{Relative Termination}

Here, one proves relative termination. Only {\sf Jambox}
participated and proved termination for 24 out of
40 examples. 

The low number of participants seems strange. 
It is safe to assume
that each termination prover contains some mechanism 
for reducing termination problems by ``removing rules''.
By making this mechanism explicit, one should obtain
a prover for relative termination with little extra work.
In turn, progress in relative termination methods and implementations
would benefit all provers.

\subsection{Context-Sensitive Termination of Term Rewriting}

Here, a lot of new developments took place in the last years. In 2006,
a dependency pair approach for context-sensitive rewriting was developed and
implemented in {\sf Mu-Term}. In 2008, this approach was improved considerably
to a context-sensitive dependency pair \emph{framework}. This framework is
implemented in {\sf AProVE} which was the only participant in
this category this year. This is a pity, since both {\sf Mu-Term} and
{\sf Jambox} also support context-sensitive rewriting (see the outermost
category above). In the future, these other tools should participate in this
category as well.
In 2008, {\sf AProVE} proved termination of 94 out of 109 examples.


