\documentclass{rtaloop}
\rtalabel{semantic-unification}


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

\begin{abstract}
Can the application condition on the \emph{Merge} rule in the computation of
dag-solved forms of unification problems be improved?
\end{abstract}

Rules are given in \cite{JK91:mit} for computing dag-solved forms of
unification problems in equational theories. The {\em Merge\/} rule $x \approx
s,x \approx t \Rightarrow x \approx s,s \approx t$ given there assumes that
$s$ is not a variable and its size is less than or equal to that of $t$. Can
this condition be improved by replacing it with the condition that the rule
{\em Check*} does not apply? (In other words, is {\em Check*} complete for
finding cycles when {\em Merge\/} is modified as above?)

\begin{remark}
The problem has been solved by Hubert Comon \cite{comon93pc} using
an extended {\em Check\/} rule (requiring a congruence closure step). 
The original question---for whatever it may be worth---stands.
\end{remark}

\end{problem}
\end{document}