\begin{slide}{Eine untere Schranke}

\emph{Fischer und Rabin 1974}:
\url{http://www.lcs.mit.edu/publications/pubs/ps/MIT-LCS-TM-043.ps}

Für \emph{jedes} Entscheidungsverfahren $E$ \\
für Presburger-Arithmetik
existiert eine Formel $F$,

so daß $E(F)$ wenigstens $2^{2^{|F|}}$
Rechenschritte benötigt.

\bigskip

Beweis-Plan: Diagonalisierung (vgl. Halteproblem):

wende solch ein Entscheidungsverfahren 
\glqq auf sich selbst\grqq\ an.

Dazu ist Kodierung nötig 
(Turing-Programm $\leftrightarrow$ Zahl)

\end{slide}

\begin{slide}{Untere Schranke}

Für Maschine $M$ und Eingabe $x$ 
sowie Funktion $f:\NN\to\NN$ (z. B. $n\mapsto 2^{2^n}$)
konstruiere Formel $D(M,x)$ mit
\begin{itemize} \itemsep 0pt
\item $D(M,x) \iff$ Maschine $M$ hält
bei Eingabe $x$ in $\le f(|x|)$ Schritten.
\item $D(M,x)$ ist klein und kann schnell berechnet
  werden.
\end{itemize}

Für jedes Entscheidungsverfahren $E$ 
für Presburger-Arithmetik: 
\begin{itemize}\itemsep 0pt
\item 
konstruiere Programm $E_0(x)$:
\\
if $E(\neg D(x,x))$ then stop else Endlosschleife.
\item
Beweise: Rechnung $E_0(E_0)$ hält nach 
$> f(|E_0|)$  Schritten.
\end{itemize}
bleibt zu zeigen, daß man solche $D$
konstruieren kann.

\end{slide}
