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

\begin{document}
\begin{problem}{Jean-Pierre Jouannaud}{}{April 1991}


\begin{abstract}
Is satisfiability of lpo or rpo ordering constraints decidable in case of
non-total precedences?
\end{abstract}

The existential fragment of the first-order theory of the ``recursive path
ordering'' (with multiset and lexicographic ``status'') is decidable when the
precedence on function symbols is total \cite{C90:lics,JO91:icalp}, but is
undecidable for arbitrary formulas. Is the existential fragment decidable for
partial precedences?


\begin{remark}
The $\Sigma_4$ ($\exists^*\forall^*\exists^*\forall^*$) fragment is
undecidable, in general \cite{treinen92jsc}. The positive existential fragment
for the empty precedence (that is, for homeomorphic tree embedding) is
decidable \cite{BC93:caap}. One might also ask whether the first-order theory
of {\em total\/} recursive path orderings is decidable. Related results
include the following: The existential fragment of the subterm ordering is
decidable, but its $\Sigma_2$ ($\exists^*\forall^*$) fragment is not
\cite{V87:jacm}. The first-order theory of encompassment (the
instance-of-subterm relation) is decidable \cite{CCD93:rta}. The
satisfiability problem for the existential fragment in the total case is
NP-complete \cite{NieuwenhuisIPL93}.

Though the first-order theory of encompassment is decidable \cite{CCD93:rta},
the first-order ($\Sigma_2$) theory of the recursive (lexicographic status)
path ordering, assuming certain simple conditions on the precedence, is not
\cite{ComonTreinen93:lri}.
\end{remark}


\end{problem}
\end{document}