\documentclass{rtaloop}
\rtalabel{one-step-theory}

\begin{document}
\begin{solvedproblem}{Hubert Comon, Max Dauchet}{}{June 1993}

\begin{abstract}
Is the first order theory of one-step rewriting decidable?
\end{abstract}

For an arbitrary finite term rewriting system $R$,
is the first order theory of one-step rewriting ($\rightarrow_R$)
decidable?
Decidability would imply the decidability of the first-order theory of
encompassment (that is, being an instance of a subterm) \cite{CCD93:rta},
as well as several known decidability results in rewriting.
(It is well known that the theory of $\rightarrow_R^*$ is in general
undecidable.) 

\begin{remark}
This has been answered negatively in \cite{Treinen:rta96,treinen98tcs}.
Sharper undecidability results have been obtained for the following
subclasses of rewrite systems:
\begin{itemize}
\item
linear, shallow, $\exists^*\forall^*$-fragment (\cite{treinen97tapsoft},
\cite{seynhaeve01tcs});
\item
linear, terminating, $\exists^*\forall^*\exists^*$-fragment
(\cite{Vorobyov:rta97}),
$\exists^*\forall^*$-fragment (\cite{Marcinkowski:rta97}).
\item
right-ground, terminating, $\exists^*\forall^*$-fragment
(\cite{Marcinkowski:rta97}).
\end{itemize}
Decidbability results have been obtained for
\begin{itemize}
\item the positive existential theory (\cite{Niehren:cade97})
\item unary signatures (\cite{Jacquemard:thesis})
\item left-linear right-ground systems (\cite{Tison:habilitation})
\end{itemize}
\end{remark}

\end{solvedproblem}
\end{document}