\documentclass{rtaloop}
\rtalabel{distributivity}

\begin{document}
\begin{solvedproblem}{J\"org Siekmann}{}{April 1991}

\begin{abstract}
Is unification modulo \emph{distributivity} decidable?
\end{abstract}

Is satisfiability of equations in the theory of distributivity (unification
modulo modulo one right- and one left-distributivity axiom) decidable? (With
just one of these, the problem had already been solved in \cite{tiden87jsc}.)
A partial positive solution is given in \cite{contejean93icalp}, based on a
striking result on the structure of certain proofs modulo distributivity.
Although many more cases are described in
\cite{contejean92these}\cite{contejean93pc}, the general case remains open.


\begin{remark}
This theory is decidable \cite{schmidt-schauss94a}\cite{schmidt-schauss:jsc97}.
\end{remark}

\end{solvedproblem}
\end{document}