\documentclass{rtaloop}
\rtalabel{ground-confluence}

\begin{document}
\begin{solvedproblem}{Wayne Snyder}{}{April 1991}

\begin{abstract}
What is the complexity of the decision problem for the confluence
of ground term-rewriting systems?
\end{abstract}

What is the complexity of the decision problem for the confluence of ground
(i.e., variable-free) term-rewriting systems? Decidability was shown in
\cite{DHLT90:ic}\cite{O87:tcs}; see also \cite{DT90:lics}.

\begin{remark}
The problem is PTIME-complete, as has been shown independently by
\cite{comon01focs} and \cite{tiwari02lics}.

\end{remark}

\end{solvedproblem}
\end{document}