Der Prozess, Entscheidungsverfahren, Axiome oder logische Theorien so zu integrieren, dass gemeinsames Schließen über heterogene Bereiche hinweg möglich ist, dabei Korrektheit und, wenn möglich, Entscheidbarkeit zu erhalten.

Prinzip

Theorien modular kombinieren durch Management gemeinsamer Signaturen, Brückenaxiome oder Kombinationstheoreme; Umgang mit Symbolteilung, Variablenäquivalenz und Modellkompatibilität sowie Anwendung geeigneter Koordinationsverfahren zur Bewahrung von Vollständigkeit und Korrektheit, wo möglich.

Demonstration

Beim automatischen Schließen erlaubt die Kombination der Theorie der linearen Arithmetik mit einer Array-Theorie die Lösung von Verifikationsbedingungen, die numerische Indizes und Array-Updates gemeinsam ansprechen, indem die beiden Theoriensolver koordiniert werden und Gleichheiten über gemeinsame Variablen ausgetauscht werden.

Fehlanwendung

Die naive Vereinigung der Axiome zweier Theorien mit überlappenden Symbolen ohne Koordination kann zu unsachgemäßen Schlüssen oder Unentscheidbarkeit führen; Theorien zu kombinieren, ohne notwendige Austauschbedingungen zu wahren, zerstört Solver-Garantien.

Konsequenz

Ermöglicht modulare Entwicklung von Solver-Architekturen und Wissensbasen und damit skalierbares Schließen über Systeme, deren Verhalten mehrere formale Domänen umfasst (z. B. Arithmetik, Datenstrukturen, temporale Beschränkungen).

Umkehrung

Isoliertes Schließen: Jede Theorie wird separat ohne Interaktion behandelt, wodurch Probleme, die integrierte semantische Informationen erfordern, nicht gelöst werden können.

Abgrenzung

Gilt, wenn die Komponententheorien und ihre Signaturen Kompatibilitätsbedingungen erfüllen (z. B. Disjunktheit oder zulässiges Teilen) und wenn Kombinationsmethoden (Nelson–Oppen-Stil, Interpolanten, explizite Axiomatisierung) anwendbar sind; schließt willkürliche Fusionen aus, die Signaturkonflikte oder modelltheoretische Inkompatibilitäten ignorieren, sowie Fälle, in denen Entscheidbarkeit unwiederbringlich verloren geht.

Semantische Spannung

Spannung zwischen flacher Kombination (durch Brückenaxiome oder Übersetzungen) und tiefer Integration (Verschmelzung axiomatischer Systeme), sowie zwischen der Wahrung der Entscheidbarkeit und der Maximierung der Ausdrucksstärke beim Kombinieren heterogener Theorien.

Synthese

Theoriekombination ist die kontrollierte Integration logischer Theorien und Entscheidungsverfahren — durch Signaturverwaltung, Austausch von Gleichheiten oder axiomatische Brücken —, um korrektes gemeinsames Schließen über heterogene Bereiche zu ermöglichen und dabei Entscheidbarkeit und Solver-Garantien zu berücksichtigen.