\documentclass{rtaloop}
\rtalabel{hermann}


\begin{document}
\begin{problem}{Miki Hermann}{}{December 1991}

\begin{abstract}
Can completion always be made terminating when limiting the depth of
occurrences of critical pairs?
\end{abstract}

Suppose ordinary completion (as in \cite{DJ90:htcs}, for example, is
non-terminating for some initial set of equations $E$, completion strategy,
and reduction ordering. Must there be a finite depth $N$ for $E$ such that for
any $n > N$ restricting the generation of critical pairs to overlaps at
positions that are no deeper than $n$ in the overlapped left-hand side (but
otherwise not changing the strategy) also produces a non-terminating
completion sequence?

\end{problem}
\end{document}