\documentclass{rtaloop}
\rtalabel{string-rewriting}
\begin{document}
\begin{solvedproblem}{Hans Zantema}{}{April 1995}
\begin{abstract}
Is it decidable whether a single term rewrite rule can be proved
terminating by a monotonic ordering that is total on ground terms?
\end{abstract}
Termination of string-rewriting systems is known to be undecidable
\cite{HL78:inria}. Termination of a single term-rewriting rule was
proved undecidable in \cite{D92,lescanne94tcs}. It is also undecidable
whether there exists a simplification ordering that proves
termination of a single term rewriting rule \cite{MG95} (cf.
\cite{JK84:rairo}). Is it decidable whether a single term rewrite
rule can be proved terminating by a monotonic ordering that is total
on ground terms? (With more rules it is not \cite{Z94open}.)
\begin{remark}
A negative solution has been given in \cite{geser97caap}. More about the
history of this problem in the context of the question of one-rule
termination can be found in \cite{Dershowitz05OpenClosed}.
\end{remark}
\end{solvedproblem}
\end{document}