\documentclass{rtaloop}
\rtalabel{gap-embedding}

\begin{document}
\begin{problem}{Nachum Dershowitz}{}{October 16, 2002}

\begin{abstract}
Design new termination methods based on the gap-embedding theorems of Friedman
and Kriz.
\end{abstract}

Harvey Friedman \cite{Simpson85a} modified Kruskal's Tree Theorem to restrict
labels that appear along the path between the images of adjacent nodes to what
is called \emph{gap embedding}. Whereas Friedman's result applied only to
labellings with the natural numbers, Igor K\v{r}\'{\i}\v{z} \cite{Kriz89}
extended it to arbitrary ordinal labellings. See also \cite{Gordeev90}. The
question is whether new and useful termination methods can be based on these
gap-embedding theorems. One step in this directions is \cite{Mizuhito95}.

This problem is related to \rtaref{graph-minors}.

\end{problem}
\end{document}