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


\begin{document}
\begin{problem}{Participants at Unif Val d'Ajol}{}{April 1991}

\begin{abstract}
Does AC unification terminate under more flexible control?
\end{abstract}

Fages \cite{F87:jsc} proved that associative-commutative unification
terminates when ``variable replacement'' is made after each step. Boudet, et
al. \cite{BCD90:lics} have proven that it terminates when variable replacement
is postponed to the end. Does the same (or similar) set of transformation
rules terminate with more flexible control?

\end{problem}
\end{document}