\documentclass{rtaloop}
\rtalabel{uniform}


\begin{document}
\begin{problem}{Hubert Comon}{}{April 1991}

\begin{abstract}
How to compute finite and complete sets of unifiers for any finitary
unification problem of a syntactic equational theory.
\end{abstract}

``Syntactic'' theories enjoy the property that a (semi\-) unification
algorithm can be derived from the axioms \cite{JK90:mit}\cite{K86:lics}. This
algorithm terminates for some particular cases (for instance, if all variable
occurrences in the axioms are at depth at most one, and cycles have no
solution) but does not in general. For the case of associativity and
commutativity (AC), with a seven-axiom syntactic presentation, the derivation
tree obtained by the non-deterministic application of the syntactic
unification rules ({\em Decompose, Mutate, Merge, Coalesce, Check*, Delete})
in \cite{JK90:mit} can be pruned so as to become finite in most cases. The
basic idea is that one unification problem (up to renaming) must appear
infinitely times on every infinite branch of the tree (since there are
finitely many axioms in the syntactic presentation). Hence, it should be
possible to prune or freeze every infinite branch from some point on. The
problem is to design such pruning rules so as to compute a finite derivation
tree (hence, a finite complete set of unifiers) for every finitary unification
problem of a syntactic equational theory.

\begin{remark}
The core of this problem has been solved \cite{boudet94ccl}.
\end{remark}

\end{problem}
\end{document}