\documentclass{rtaloop}
\rtalabel{ord-constraints-plus}


\begin{document}
\begin{problem}{Hubert Comon, Robert Nieuwenhuis}{}{January 1998}

\begin{abstract}
Is the satisfiablity of ordering constraints (lpo) in conjunction with
predicates like irreducibility by a fixed rewrite system or membership
in a regular tree language decidable?
\end{abstract}

Satisfiability of ordering constraints (lpo) for total precedences
has been shown decidable
in \cite{C90:lics,NieuwenhuisIPL93}. Is the satisfiablity
of total lpo ordering constraints together with the constraint
$Irr(x)$, expressing that $x$ is not reducible by some fixed rewrite
system, decidable? This would imply decidability of
the confluence of ordered rewriting (see \rtaref{ordered}).

Besides the irreducibility predicate the following related predicates
are of interest:
\begin{itemize}
\item membership in a fixed regular tree language
\item a predicate expressing that a fixed symbol does not occur in a term.
\end{itemize}

\end{problem}
\end{document}