\documentclass{rtaloop}
\rtalabel{constraint}


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

\begin{abstract}
Design a framework for combining constraint solving algorithms.
\end{abstract}

Design a framework for combining constraint solving algorithms.

\begin{remark}
Some particular cases have been attacked: In \cite{BS92:cade} it was shown how
decision procedures for solvability of unification problems can be combined.
In \cite{BS93:rta} a similar technique is applied to (unquantified) systems of
equations and disequations. In \cite{R92:lpar} the combination of unification
algorithms is extended to the case where alphabets share constants. In related
work \cite{B92:cade}, unification is performed in the combination of an
equational theory and membership constraints.

Some further progress is in \cite{R92:lpar}.

The combination approach of \cite{BS92:cade} has been extended in
\cite{BaaderSchulz-RTA-95} to constraints involving predicate symbols other
that equality, and \cite{BaaderSchulz-CP-95} in turn extends this approach to
constraint-solving over solution domains that are not free structures. These
results are presented in a uniform framework by \cite{BaaderSchulz-TCS-98}.

The work of \cite{R92:lpar} has been extended
to the case of ``shared constructors'' by~\cite{DomenKRCADE94}.
\end{remark}

\begin{submitted}{Miki Hermann}{Mon Apr 27 12:05:20 MET DST 1998}

Unification algorithms (and therefore also constraint solvers) cannot be
combined in polynomial time, as proved by Hermann and Kolaitis
in~\cite{HermannKolaitis96cade}.

\end{submitted}

\end{problem}
\end{document}