Nelson-Oppen für konvexe Theorien

für entscheidbare Theorien T₁,…, T_n mathend000# (jeweils T_i mathend000# über Σ_i mathend000#)

• Eingabe: gereinigte Formel φ = φ₁∧…∧φ_n mathend000#

  (mit φ_i mathend000# über Σ_i mathend000#)

• wenn ein φ_i mathend000# nicht erfüllbar, dann ist φ mathend000# nicht erfüllbar
• wenn T_i $\models$ (φ_i→x_i = y_i) mathend000#, dann Gleichung x_i = y_i mathend000# zu allen φ_j mathend000# hinzufügen,...
• bis sich nichts mehr ändert, dann φ mathend000# erfüllbar

(Beispiele)

(Beweis)