\begin{slide}{Zusammenfassung Entscheidbarkeit}

durch Automaten-Operationen sind realisierbar:

\begin{itemize}
\item elementare Relationen ($x+y=z$)
\item Quantoren und logische Verknüpfungen
\end{itemize}

Folgerungen
\begin{itemize}
\item 
 zu jeder Presburger-Formel $F$
kann ein Automat $A$ konstruiert werden
mit $\Mod(F)=\Lang(A)$.
\item
 Allgemeingültigkeit,
Erfüllbarkeit, Widersprüchlichkeit 
von Presburger-Formel ist entscheidbar.
\end{itemize}

die Komplexität des hier angegeben 
Entscheidungsverfahrens ist hoch, geht das besser?

\end{slide}
