\documentclass{rtaloop}
\rtalabel{negation}

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

\begin{abstract}
Can negations be effectivly eliminated from first-order formulas over trees,
where equality is the only predicate?
\end{abstract}

Given a first-order formula with equality as the only predicate symbol, can
negation be effectively eliminated from an arbitrary formula $\phi$ when
$\phi$ is equivalent to a positive formula? Equivalently, if $\phi$ has a
finite complete set of unifiers, can they be computed? Special cases were
solved in \cite{C88:grenoble,LM87:jar}.

\begin{remark}
A positive solution is given in \cite{T93:rta}.
\end{remark}

\end{solvedproblem}
\end{document}