\section{String Rewriting}\label{subsec:srs}


These categories are similar to the TRS categories, but here one only regards
TRSs where the function symbols have arity 1. 
Again, it is a pity that many of the tools that have been working on string
rewrite systems in the past did not participate in the competition in 2008.

The previous winner {\em Matchbox} did participate in the certified
string rewriting category instead. Recent progress in
certification has narrowed the gap between the results in
these two categories, see the discussion in Section~\ref{sec:cert}.

For full termination of SRSs,
the tools \TTTT and {\sf AProVE}
that used to be tailored more to general TRSs than to SRSs
were the most powerful ones. It is unclear whether this is due to the fact
that tools which are more tailored to SRSs did not participate in this
category in 2008 or whether the TRS-tools really improved so much on SRSs.

The winner for proving termination 
in this category was \TTTT which proved termination for 512
SRSs and disproved it for 40 followed by {\sf AProVE} which proved termination
for 501 and disproved it for 22 SRSs.  {\sf Jambox} proved termination of 252
SRSs.
For disproving termination of SRSs, the new tool {\sf nonloop} was the winner
by disproving termination of 92 SRSs. In particular, this tool is the first to
also prove non-termination of some non-looping SRSs,
by enumerating patterns in (forward) closures,
and checking whether they are recurrent.
\TTTT\ finds loops by encoding derivations as
a Boolean constraint system.

For relative termination of SRSs, only {\sf Jambox}
participated and proved termination for 32 out of
42 examples.

