\documentclass{rtaloop}
\rtalabel{ac}

\begin{document}
\begin{solvedproblem}{Ralf Treinen}{\cite{T90:fst}}{April 1991}

\begin{abstract}
Is the $\Sigma_2$-fragment of the first-order theory of ground terms 
modulo AC decidable?
\end{abstract}

Consider a finite set of function symbols containing at least one AC 
(associative-commutative) function symbol. Let $T$ be the corresponding set
of terms (modulo the AC properties).
It is known from \cite{treinen92jsc} that the first-order theory ($\Sigma_3$
fragment) of $T$ is undecidable when $F$ contains at least a
non-constant symbol (besides the AC symbol). 
When $F$ only contains an AC symbol and constants, 
the theory reduces to Presburger's arithmetic and is hence decidable.
On the other  hand the $\Sigma_1$ fragment of $T$ is always decidable
\cite{comon93tcs}.
The decidability of the $\Sigma_2$ fragment of the theory of $T$
remains open.  


\begin{remark}
Even more, the solvability of the following important
particular case is open: given $t,t_1,\ldots,t_n \in T(F,X)$, is there
an instance of $t$ which is not an instance of $t_1,\ldots,t_n$ modulo
the AC axioms? This is known as {\em complement problems} modulo AC. 

Several special cases have been solved \cite{F93:rta}\cite{LM93:stacs},
and in unpublished work in progress.

The undecidability of the $\Sigma_2$-fragment of the first-order theory 
of ground terms modulo AC has been shown by~\cite{Marcinkowski:rta99}.
\end{remark}

\end{solvedproblem}
\end{document}