\documentclass{rtaloop}
\rtalabel{combining}

\begin{document}
\begin{problem}{Franz Baader, Klaus Schulz}{\cite{BS92:cade}}{June 1993}

\begin{abstract}
Investigate the exact difference between \emph{linear constant restrictions}
and \emph{arbitrary constant restrictions} in unification problems.
\end{abstract}

It was shown in \cite{BS92:cade} that being able to solve
unification problems with linear constant restrictions is a
necessary and sufficient condition
for the possibility of combining unification
algorithms. Other approaches 
\cite{SchmidtSchaussCombination}\cite{BoudetCombination} require 
solvability of constant elimination problems, which was
shown to be 
equivalent to presupposing solvability of unification problems with
arbitrary constant restrictions \cite{BS92:cade}.
Is there an equational theory for which solvability of unification
problems with linear constant restrictions is decidable, but solvability
of unification problems with arbitrary constant restrictions is
undecidable?
Is there an equational theory for which unification
problems with linear constant restrictions always have a finite complete
set of solutions, but unification problems with arbitrary constant 
restrictions sometimes don't?



\end{problem}
\end{document}