\documentclass{rtaloop}
\rtalabel{existential}

\begin{document}
\begin{solvedproblem}{Hubert Comon}{}{June 1993}

\begin{abstract}
Is satisfiability of \emph{set constraints with projection and boolean
operators} decidable?
\end{abstract}

Consider the existential fragment of the theory
defined by a binary predicate symbol $\subseteq$, a finite
set of function symbols $f_1,\ldots, f_n,$ the function
symbols $\cap, \cup, \neg$, and the projection symbols 
$f_{i,j}^{-1}$ for $j \leq arity(f_i)$. 
Variables are interpreted as subsets of the Herbrand Universe.
With the obvious interpretation of these symbols, is satisfiability
of such formulas decidable?
Special cases have been solved in
\cite{HJ90:lics,AW92:lics,BGW93:lics,GTT93:stacs}.


\begin{remark}
This has been solved positively by
\cite{CharatonikPacholski-focs94}.

Partial solutions have been given by
\cite{gilleron93focs}\cite{charatonik94lics}\cite{aiken93cornell}.
\end{remark}

\end{solvedproblem}
\end{document}