\documentclass{rtaloop}
\rtalabel{ordered-completeness}

\begin{document}
\begin{solvedproblem}{Nachum Dershowitz, Jean-Pierre Jouannaud}{}{April 1991}

\begin{abstract}
  Is there a set of inference rules that always succeeds in computing a
  convergent set of rewrite rules for a given set of equations and an
  ordering, provided that it exists?
\end{abstract}

Ordered rewriting computes a given convergent set of rewrite rules for an
equational theory $E$ and an ordering $>$ whenever such a set $R$ exists for
$>$, provided $>$ can be made total on ground terms. Unfortunately, this is
not always possible, even if $>$ is derivability ($\rightarrow_R^+$) in $R$.
Is there a set of inference rules that will always succeed in computing $R$
whenever $R$ exists for $>$?

\begin{remark}
  A proposal appears in \cite{Devie-thesis}; more work is called for.
  
  A positive answer has been given in \cite{bofill:lics99}.
\end{remark}

\end{solvedproblem}
\end{document}