\documentclass{rtaloop}
\rtalabel{higher-order}

\begin{document}
\begin{solvedproblem}{Tobias Nipkow, Masako Takahashi}{}{June 1993}

\begin{abstract}
Are weakly orthogonal higher-order rewrite systems confluent?
\end{abstract}

For higher-order rewrite formats as given by combinatory
reduction systems \cite{K80:mct} and higher-order rewrite systems
\cite{N91:lics,T93:tlca},
confluence has been proved in the restricted case of
orthogonal systems.  Can confluence be extended to
such systems when they are weakly orthogonal (all critical pairs are trivial)?
When critical pairs arise only at the root,
confluence is known to hold. 

\begin{remark}
Weakly orthogonal higher-order rewriting systems are confluent.
This has been shown both via the Tait-Martin-L\"of method and
via finite developments \cite{Oost:Raam:94}.

The details and further extensions similar to Huet's parallel closure
condition can be found in \cite{Oostrom-PhD,Oostrom-TCS97,Raamsdonk-PhD}.
\end{remark}

\end{solvedproblem}
\end{document}