\documentclass{rtaloop}
\rtalabel{constants}


\begin{document}

\begin{solvedproblem}{Franz Baader, Klaus Schulz}{}{}

  \begin{abstract}
    Is there an equational theory for which unification with constants is
    decidable, but general unification is undecidable?
  \end{abstract}
  

  Is there an equational theory for which unification with constants
  is decidable, but general unification (where free function symbols
  of arbitrary arity may occur) is undecidable?  From the results in
  \cite{BS92:cade} it follows that this question can be reformulated
  as follows: Is there an equational theory for which unification with
  constants is decidable, but unification with linear constant
  restrictions is undecidable?  Another way of formulating the
  question is: Consider {\em positive} first-order
  formul\ae\ containing equality as the only predicate symbol, and
  function symbols from a given alphabet $\cal F$.  Is there an
  equational theory $E$ with alphabet $\cal F$ such that whether $E
  \models \phi$ is decidable for closed formulae $\phi$ with
  quantifier prefix $\forall^\ast\exists^\ast$, but undecidable for
  arbitrary quantifier prefixes?

  \begin{remark}
    This has been answered in the affirmative \cite{otop12jar} by exhibiting
    such an equational theory.
  \end{remark}
  
\end{solvedproblem}

\end{document}