\documentclass{rtaloop}
\rtalabel{one}

\begin{document}
\begin{problem}{Max Dauchet}{}{April 1991} 

\begin{abstract}
  Is termination of one linear rule decidable?
\end{abstract}

Is termination of one linear (left and right) rule decidable? Left linearity
alone is not enough for decidability \cite{D89:rta}.

\begin{remark}
  A less ambitious, long-standing open problem (mentioned in \cite{DJ90:htcs})
  is decidability for {\em one\/} (length-increasing) monadic (string,
  semi-Thue) rule. Termination is undecidable for non-length-increasing
  monadic systems of rules \cite{C91:caap}. For one monadic rule, confluence
  is decidable \cite{K90:tuc}\cite{W90:wert}. What about confluence of one
  non-monadic rule?

  Partial results for string rewrite rules have been obtained in
  \cite{geser03rta}.

  The history of the problem and the attempts to solve it are told in
  \cite{Dershowitz05OpenClosed}.
\end{remark}

\end{problem}
\end{document}
