\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}