Nelson-Oppen für konvexe Theorien

für entscheidbare Theorien T₁,..., T_n:

• Eingabe: gereinigte Formel $\phi$ = $\phi_{1}^{}$ $\wedge$...$\wedge$ $\phi_{n}^{}$
• wenn ein $\phi_{i}^{}$ nicht erfüllbar, dann ist $\phi$ nicht erfüllbar
• wenn T_i $\models$ ($\phi_{i}^{}$$\to$x_i = y_i), dann Gleichung x_i = y_i zu allen $\phi_{j}^{}$ hinzufügen,...
• bis sich nichts mehr ändert, dann $\phi$ erfüllbar

(Beispiele)

(Beweis)