\begin{slide}{Folgerungen aus Unentscheidbarkeit}

Suche nach (effizienten) Algorithmen für Spezialfälle

(die trotzdem ausreichen, um interessante Anwendungsprobleme
zu modellieren)

\begin{itemize} \itemsep 0pt
\item Einschränkung der Signatur (Bsp: keine F.-S.,
nur einstellige F.-S, nur einstellige Rel.-S.)
\item Einschränkung der Formelsyntax
  \begin{itemize}
  \item nur bestimmte Quantoren, 
    nur an bestimmten Stellen

    (im einfachsten Fall: ganz außen existentiell)
  \item nur bestimmte Verknüpfungen (Bsp: nur durch $\wedge$)
  \end{itemize}
\item Einschränkung auf Theorien von gegebenen Strukturen

  Bsp: $F\in\Th(\NN,0,+)$? Theorie der ganzen Zahlen mit Addition
\end{itemize}

\end{slide}
