\documentclass{rtaloop}
\rtalabel{conditional-termination}


\begin{document}
\begin{solvedproblem}{Nachum Dershowitz}{}{April 1991}

\begin{abstract}
Devise practical methods for proving termination of conditional rewriting
systems.
\end{abstract}

Devise practical methods for proving termination of (standard) conditional
rewriting systems.  Part of the difficulty stems from the interdependence of
normalization and termination.

\begin{remark}
Termination and decreasingness of CTRSs can be proved by transforming CTRSs
into unconditional TRSs such that termination of the TRS is sufficient for
decreasingness of the CTRS. Several variants of this transformation are
studied in \cite{BK86:jcss,DP86,GA01,GM87,Sivakumar89:uiuc,M96,O01}.
Termination of the TRSs resulting from this transformation can often be proved
automatically using dependency pairs \cite{AG00,GA01}. The transformation
(together with the dependency pair approach) is implemented in the tools
\ahref{http://bibiserv.techfak.uni-bielefeld.de/talp/}{{\sf TALP}} \cite{TALP}
and \ahref{http://www-i2.informatik.rwth-aachen.de/AProVE/}{{\sf AProVE}}
\cite{AProVE}. Both tools use this transformation in order to show termination
of logic programs, but {\sf AProVE} can also prove termination and
decreasingness of CTRSs in this way. A different approach for termination
proofs of CTRSs with the general path order \cite{DH95} is described in
\cite{HootPhD}.
\end{remark}

\end{solvedproblem}
\end{document}