\documentclass{rtaloop}
\rtalabel{aci}

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

\begin{abstract}
  How can completion modulo ACUI be made effective?
\end{abstract}

Completion modulo associativity and commutativity (AC) \cite{PS81:jacm} is
probably the most important case of \emph{extended completion}; the general
case of finite congruence classes is treated in \cite{JK86:siam}. Adding an
axiom (U) for an identity element ($x+0=x$) gives rise to infinite classes.
This case was viewed as conditional completion in \cite{BPW89}, and solved
completely in \cite{JM89:disco}. The techniques, however, do not carry over to
completion with idempotence (I) added ($x+x=x$). How to handle ACUI-completion
effectively is open.

\begin{remark}
  \emph{Normalized Rewriting} as introduced by Claude March\'e in
  \cite{marche96jsc} is the right way of handling axiom systems like ACUI.
\end{remark}

\end{solvedproblem}
\end{document}