Definition

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

Kombination von Theorien:

• Theorie T₁ über $\Sigma_{1}^{}$, Theorie T₂ über $\Sigma_{2}^{}$.
• Theorie T₁ $\oplus$ T₂ über $\Sigma_{1}^{}$ $\cup$ $\Sigma_{2}^{}$

Aufgabenstellung:

• gegeben: Entscheidungsverfahren (Constraint-Solver) für T₁, T₂ (einzeln)
• gesucht: ...für T₁ $\oplus$ T₂