\documentclass{rtaloop}
\rtalabel{ordered}

\begin{document}
\begin{problem}{Nachum Dershowitz}{}{June 1993} 

\begin{abstract}
Is confluence of ordered rewriting decidable when the (existential fragment of
the) ordering is? 
\end{abstract}

Is confluence of ordered rewriting (using the intersection of one step
replacement of equals and a reduction ordering that is total on ground terms)
decidable when the (existential fragment of the) ordering is?
This question was raised in \cite{nieuwenhuis93rta},
where some results were given for the lexicographic path ordering.

\begin{remark}
This was answered positive for the  case of lexicographic path orderings,
which is probably the most important special case,
in \cite{CNNR:lics98}.
The general question, however, remains open.
\end{remark}

\end{problem}
\end{document}