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