\documentclass{rtaloop}
\rtalabel{occur-check}


\begin{document}
\begin{problem}{Mizuhito Ogawa}{}{April 1995}

\begin{abstract}
  Does a system that is nonoverlapping under unification with infinite
  terms have unique normal forms?
\end{abstract}
Does a system that is nonoverlapping under unification with infinite
terms (unification without ``occur-check'' \cite{Martelli:84}) have
unique normal forms? This conjecture was originally proposed in
\cite{OgawaOno:89} with an incomplete proof, as an extension of the
result on strongly nonoverlapping systems
\cite{K80:mct}\cite{C81:stoc}.  Related results appear in
\cite{OO93:ieice}\cite{Toyama94}\cite{ManoOgawa:94}, but the original
conjecture is still open.  This is related to Problem 58.  This
problem is also related with modularity of confluence of systems
sharing constructors, see \cite{ohlebusch94}.
\begin{remark}
  The answer is yes if the system is also nonduplicating \cite{Rak96}.
  A direct technique is given in \cite{Rak96}.  The nonduplicating
  condition can be relaxed under a certain technical condition
  \cite{Rak96}. Some extensions to handle root overlaps are given in
  \cite{Rak97} and a restricted version of the result in
  \cite{C81:stoc} is also proved using the direct technique in
  \cite{Rak97}.
\end{remark}
\end{problem}
\end{document}