\documentclass{rtaloop}

\begin{document}
\begin{problem}{Jürgen Giesl and Hans Zantema}{}{July 2010}

  \begin{abstract}
     Can we use the dependency pair method to prove relative termination?
  \end{abstract}

  The key of the success of the dependency pair method in proving
  termination is the following property from \cite{AG00,giesl06jar}, stated
  in more recent terminology:
  \begin{quote}
    A TRS $R$ is terminating if and only if the dependency pair problem
    $(DP(R),R)$ is terminating.
  \end{quote}
  A dependency pair problem is a pair $(P,R)$ of TRSs. Such a
  dependency pair problem is called terminating if it admits no
  infinite chain, that is, there is no $P \cup R$ reduction containing
  infinitely many $P$-steps, where $P$-steps only occur at the root.

  Can we use the dependency pair method to prove relative termination?
  Here for a pair $(R,S)$ of TRSs, $R$ is said to be terminating
  modulo $S$ if there is no $R \cup S$ reduction containing infinitely
  many $R$-steps. This is the same requirement as for termination of a
  dependency pair problem, except that the first TRS in a dependency
  pair problem may only be used for root steps. So, more precisely,
  the open problem is:

  \begin{quote}
    Find a ``useful'' effectively computable function $\phi$ from pairs
    of TRSs to dependency pair problems, such that for every two TRSs
    $R,S$ the TRS $R$ is terminating modulo $S$ if and only if the
    dependency pair problem $\phi(R,S)$ is terminating.
  \end{quote}
  
  Here, ``useful'' means that the resulting dependency pair problem
  $\phi(R,S)$ should be ``easy'' (i.e., suitable for automated
  termination analysis by existing tools).
  
\end{problem}

\end{document}