(Wdhlg) Signatur Σ
mathend000#, Theorie T
mathend000#,
Gültigkeit
T
φ
mathend000#
Kombination von Theorien:
- ...mit disjunkten Signaturen:
Σ1∩Σ2 = ∅
mathend000#
- Theorie T1
mathend000# über Σ1
mathend000#,
Theorie T2
mathend000# über Σ2
mathend000#.
- Theorie
T1⊕T2
mathend000#
über
Σ1∪Σ2
mathend000#
Aufgabenstellung:
- gegeben: Constraint-Solver
(Entscheidungsverfahren)
für T1
mathend000#,
Constraint-Solver für T2
mathend000#;
- gesucht: Constraint-Solver für
T1⊕T2
mathend000#
2014-03-31