\documentclass{rtaloop}
\rtalabel{allegories-unif}


\begin{document}
\begin{problem}{Dan Dougherty}{(Talk at RTA 2000)}{July 2000}

\begin{abstract}
Is unification modulo the theory of allegories decidable?
\end{abstract}

Let {\it ALL} be the equational theory of Allegories.
Is unification modulo {\it ALL} decidable?

Background: 

The notion of "Allegory" has defined by Peter Freyd and Andre Scedrov
in their monograph \cite{FreydScedrov:allegories}.  Allegories are to
binary relations between sets as categories are to functions between
sets.  By ALL we refer to the untyped version of the theory (see page
195 of \cite{FreydScedrov:allegories}).

Validity in this equational theory is decidable (Guti\'errez'
dissertation, Wesleyan University 1999, also see \cite{dougherty:rta00}).
The universal-existential theory over these axioms is undecidable
(reduction from the universal-existential theory of free semigroups
with constants).

\end{problem}
\end{document}