\documentclass{rtaloop}
\rtalabel{graph-minors}


\begin{document}
\begin{problem}{Jean-Claude Raoult}{}{June 1993}

\begin{abstract}
  Find an embedding theorem for directed graphs.
\end{abstract}
Termination is, as we know, undecidable. Yet, there are several
sufficient conditions ensuring termination for word and term
rewritings. Most are suitable extensions of Higman's or Kruskal's
embeddings \cite{K60:tams}.  Robertson and Seymour \cite{RS82:osu}
have achieved a similar theorem for undirected graphs.  However, no
embedding theorem has yet been proved for directed graphs, and
(consequently?) powerful termination orderings remain to be designed.

This problem is related to \rtaref{gap-embedding}.

\begin{remark}
In \cite{RobertsonSeymour:96},
embedding theorems are proved for directed wqo-labelled graphs and
hypergraphs.
\end{remark}

\begin{submitted}{Bruno Courcelle}{Mon, 31 Jan 2005 10:20:21 +0100}
  Graph rewriting termination: it is usually no problem because there is no
  duplication of subgraph, and the size reduces. One can of course interpret a
  term rewriting system as a graph rewriting system, if the symbols of the
  term denote graph operations. Hence, the termination is handled at the level
  of terms, with the well-known tools and criteria.
\end{submitted}
\end{problem}
\end{document}