\begin{slide}{Termination Problem Semantics}

  \begin{itemize}
  \item input: 
    \begin{itemize}
    \item (an effective description of a)

      binary relation $\to$  (a step of a computation)
    \end{itemize}
  \item questions:
    \begin{itemize}
    \item termination: $\to$ is well-founded
    \item derivational complexity: length of $\to$-chains
    \end{itemize}
  \item answers (yes, no, lower/upper bounds)
    \begin{itemize}
    \item for human inspection
    \item for automated verification
    \end{itemize}
  \end{itemize}

\end{slide}

\overlays{3}{
\begin{slide}{What Computations?}
  \begin{itemize}\itemsep 2pt
  \item functional program  (Haskell)
  \item logic program (Prolog)
  \item \fromSlide{2}{
      \emph{coming:} imperative programs (Java Bytecode)
    }
  \item rewrite system
    \begin{itemize}\itemsep 2pt
    \item unary/arbitrary signature (SRS/TRS)
    \item strategy (none, inner/outermost, contextsens.)
    \item start terms (all, constructor-based)
    \item relative/equational: $\to_1 \circ \to_2^*, \to_1 \circ \leftrightarrow_2^*$ \\
      instances: $\leftrightarrow_2^*$ for A, C, I
    \end{itemize}
  \item \fromSlide{3}{
      \emph{coming:} background theories (integers,\dots)
    }
  \end{itemize}
\end{slide}
}