\documentclass{rtaloop}
\rtalabel{existential-onestep-theory}


\begin{document}
\begin{problem}{Ralf Treinen}{\cite{Treinen:rta96}}{1996}

\begin{abstract}
Are the existential fragment or the positive fragment
of the theory of one-step rewriting decidable?
\end{abstract}

For a given signature $\Sigma$ and rewrite system $R$, the theory
of one-step rewriting by $R$ is the first order theory of the model
comprising all $\Sigma$-ground-terms, and the binary predicate
{\it $x$ rewrites to $y$ in one rewrite step of $R$}.

It is well-known that
the full first-order theory is undecidable, even for strong restrictions
on the class of rewrite systems (see \rtaref{one-step-theory}). Is the
existential fragment of this theory (in other words: satisfiability
of quantifier-free formulas) decidable?
Is the positive fragment (arbitrary quantification, but no negation or implications) decidable?

It is known that the positive existential fragment
is decidable \cite{Niehren:cade97},
and there are decidability results for the full existential fragment
in case of restricted classes of rewrite
systems \cite{Caron:rta99,Limet:rta99}.

\end{problem}
\end{document}