\documentclass{rtaloop}
\rtalabel{rewriting-decidability}

\begin{document}
\begin{problem}{Albert Meyer}{}{April 1991}


\begin{abstract}
Is there a decidable uniform word problem for which there is no variant on the
rewriting theme that can decide it---without adding new symbols?
\end{abstract}

Is there a decidable uniform word problem for which there is no variant on the
rewriting theme (for example, rewriting modulo a congruence with a decidable
matching problem, or ordered rewriting) that can decide it---without adding
new symbols to the vocabulary? There are decidable theories that cannot be
decided with ordinary rewriting (see, for example, \cite{Squier1987a}); on the
other hand, any theory with decidable word problem can be solved by
ordered-rewriting with some ordered system for some conservative extension of
the theory (that is, with new symbols) \cite{DMT85:aero}, or with a two-phased
version of rewriting, wherein normal forms of the first system are inputs to
the second \cite{B85:tcs}.

\end{problem}
\end{document}