\documentclass{article}
\usepackage{amsmath,amssymb,amsfonts}
\parindent0em
\setlength{\textwidth}{18cm}
\setlength{\textheight}{23cm}
\hoffset-3.5cm
\begin{document}
\Large
\begin{center}
    Zum Satz von Savitch
\end{center}
\textit{Gegeben}: Graph $G = (V,E)$ mit $V = \{1,2,\ldots,n\}$ 
und Knoten $u,v \in V$\\[3mm]
\textit{Problem}: Gibt es einen Pfad in $G$ von $u$ nach $v$\\[3mm]
\textit{Pr\"adikat}:
\[
\text{PATH}(x,y,m) :=
\hbox{es gibt in $G$ einen Pfad der L\"ange $\leq m$
von $u$ nach $v$} ?
\]
\textit{Tatsache}:
\begin{align*}
\text{PATH}(x,y,2^k)
&~\Leftrightarrow~
\exists z \left(
\text{PATH}(x,z,2^{k-1}) \wedge
\text{PATH}(z,y,2^{k-1}) \right)~~~(k > 0)\\[3mm]
\text{PATH}(x,y,2^0)
& ~\Leftrightarrow~
x=y \vee (x,y) \in E
\end{align*}

\pagebreak

\begin{center}
    Zur Implementierung des Algorithmus von Savitch
\end{center}

activation records:
\begin{align*}
    (x,y,k) &\leftrightarrow \text{PATH}(x,y,2^k)~\hbox{is}~\mathtt{goal}\\
    \overline{(x,y,k)}
    &\leftrightarrow
    \text{PATH}(x,y,2^k)~\hbox{is}~\mathtt{true}\\
    \underline{(x,y,k)}
    &\leftrightarrow
    \text{PATH}(x,y,2^k)~\hbox{is}~\mathtt{false}
\end{align*}

\bigskip

Aktuelle Liste (stack) der activation records:
\[
(x_{0},y_{0},d)(x_{1},y_{1},d-1) \cdots (x_{k-1},y_{k-1},d-k+1)(x_{k},y_{k},d-k)
\]
wobei der letzte record auch 
$\underline{(x_{k},y_{k},d-k)}$ oder 
$\overline{(x_{k},y_{k},d-k)}$ sein kann

\bigskip

Transitionen:
\begin{align*}
    (x,y,k) ~~&\vdash~~ (x,y,k)(x,1,k-1) &\\
    (x,y,k)\overline{(x,z,k-1)} ~~&\vdash~~ (x,y,k)(z,y,k-1) &\\
    (x,y,k)\overline{(z,y,k-1)} ~~&\vdash~~ \overline{(x,y,k)} &\\
    (x,y,k)\underline{(x,z,k-1)} ~~&\vdash~~ (x,y,k)(x,z+1,k-1) & (z < n)\\
    (x,y,k)\underline{(x,n,k-1)} ~~&\vdash~~ \underline{(x,y,k)} &\\
    (x,y,k)\underline{(z,y,k-1)} ~~&\vdash~~ (x,y,k)(x,z+1,k-1) & (z < n)\\
    (x,y,k)\underline{(n,y,k-1)} ~~&\vdash~~ \underline{(x,y,k)} &\\
\end{align*}

Elementare Situation
\[
(x,y,0) ~~\vdash~~ 
\begin{cases}
    \overline{(x,y,0)} & \text{falls}~x=y~\text{oder}~(x,y) \in E\\
    \underline{(x,y,0)} & \text{sonst}
\end{cases}
\]

Startliste
\[
(u,v,d)~~\text{mit}~~d = \lceil \log (n-1) \rceil
\]

Endliste
\begin{align*}
    \overline{(u,v,d)} &~~\text{falls}~ \text{PATH}(u,v,d)~\mathtt{true}\\
    \underline{(u,v,d)} &~~\text{falls}~\text{PATH}(u,v,d)~\mathtt{false}
\end{align*}
\end{document}