\begin{slide}{Nelson-Oppen für konvexe Theorien}
für entscheidbare Theorien $T_1,\ldots,T_n$
(jeweils $T_i$ über $\Sigma_i$)

  \begin{itemize}
  \item Eingabe: 
    gereinigte Formel 
    $\phi= \phi_1\wedge\ldots\wedge\phi_n$
    
    (mit $\phi_i$ über $\Sigma_i$)
  \item wenn ein $\phi_i$ nicht erfüllbar,
    dann ist $\phi$ nicht erfüllbar
  \item wenn $T_i \models (\phi_i \to x_i=y_i)$,
    dann Gleichung $x_i=y_i$ 
    zu allen $\phi_j$ hinzufügen,\dots
  \item bis sich nichts mehr ändert,
    dann $\phi$ erfüllbar
  \end{itemize}

(Beispiele)

(Beweis)

\end{slide}
