\documentclass{rtaloop}
\rtalabel{extended}


\begin{document}
\begin{problem}{Deepak Kapur}{}{December 1991}

\begin{abstract}
For which equational theories is ground reducibility of extended rewriting
decidable? 
\end{abstract}

Ground reducibility of extended rewrite systems, modulo congruence, like
associativity and commutativity (AC), is undecidable \cite{KNZ87:acta}. For
left-linear AC systems, on the other hand, it is decidable \cite{JK89:ic}.
What can be said more generally about restrictions on extended rewriting that
give decidability? This problem is related to \rtaref{ac}.

\begin{remark}
Progress has been made in \cite{KuchRusi94a}, where it is proven that ground
reducibility remains undecidable when a single non-constant function symbol is
associative.
\end{remark}

\end{problem}
\end{document}