\begin{slide}{Definition}

(Wdhlg) Signatur $\Sigma$, Theorie $T$,
Gültigkeit $T \models \phi$

Kombination von Theorien:
\begin{itemize}
\item \dots mit disjunkten Signaturen: 
  $\Sigma_1\cap\Sigma_2=\emptyset$
\item Theorie $T_1$ über $\Sigma_1$,
  Theorie $T_2$ über $\Sigma_2$.
\item Theorie $T_1 \oplus T_2$
  über $\Sigma_1 \cup \Sigma_2$
\end{itemize}

Aufgabenstellung:
\begin{itemize}
\item gegeben:   Constraint-Solver
(Entscheidungsverfahren)
für $T_1$,
  Constraint-Solver für $T_2$;
\item gesucht: Constraint-Solver für $T_1 \oplus T_2$
\end{itemize}

\end{slide}
