Definition

(Wdhlg) Signatur Σ mathend000#, Theorie T mathend000#, Gültigkeit T $\models$ φ mathend000#

Kombination von Theorien:

• ...mit disjunkten Signaturen: Σ₁∩Σ₂ = ∅ mathend000#
• Theorie T₁ mathend000# über Σ₁ mathend000#, Theorie T₂ mathend000# über Σ₂ mathend000#.
• Theorie T₁⊕T₂ mathend000# über Σ₁∪Σ₂ mathend000#

Aufgabenstellung:

• gegeben: Constraint-Solver (Entscheidungsverfahren) für T₁ mathend000#, Constraint-Solver für T₂ mathend000#;
• gesucht: Constraint-Solver für T₁⊕T₂ mathend000#