Le processus d'intégration de procédures de décision, d'axiomes ou de théories logiques afin de permettre un raisonnement conjoint à travers des domaines hétérogènes tout en préservant la correction et (si possible) la décidabilité.

Principe

Combiner les théories de manière modulaire en gérant signatures partagées, axiomes-pont ou théorèmes de combinaison ; traiter le partage de symboles, l'égalité des variables et la compatibilité des modèles, et appliquer des méthodes de coordination adaptées pour maintenir, lorsque possible, l'exhaustivité et la correction.

Démonstration

En raisonnement automatique, combiner une théorie de l'arithmétique linéaire avec une théorie des tableaux permet de résoudre des conditions de vérification mentionnant à la fois des indices numériques et des mises à jour de tableaux en coordonnant les solveurs des deux théories et en échangeant des égalités sur les variables partagées.

Mauvaise application

Prendre naïvement l'union des axiomes de deux théories avec symboles chevauchants sans coordination peut conduire à des inférences non fondées ou à la perte de décidabilité ; combiner des théories sans préserver les conditions d'échange requises détruit les garanties des solveurs.

Conséquence

Permet le développement modulaire de solveurs et de bases de connaissances, autorisant un raisonnement évolutif sur des systèmes dont le comportement couvre plusieurs domaines formels (par exemple arithmétique, structures de données et contraintes temporelles).

Inversion

Raisonnement isolé : chaque théorie est traitée séparément sans interaction inter-théories, empêchant la résolution de problèmes qui exigent une information sémantique intégrée.

Limite

S'applique lorsque les théories composantes et leurs signatures satisfont des conditions de compatibilité (par exemple disjonction ou partage admissible) et lorsque des méthodes de combinaison (style Nelson–Oppen, interpolants, axiomatation explicite) sont appropriées ; exclut les fusions arbitraires qui ignorent les conflits de signatures ou les incompatibilités modèle-théoriques et les cas où la décidabilité est irrémédiablement perdue.

Tension sémantique

Tension entre combinaison superficielle (via axiomes-pont ou traductions) et intégration profonde (fusionner les systèmes d'axiomes en une seule théorie), ainsi qu'entre la préservation de la décidabilité et la maximisation de l'expressivité lors de la combinaison de théories hétérogènes.

Synthèse

La combinaison de théories est l'intégration contrôlée de théories logiques et de procédures de décision — par gestion des signatures, communication d'égalités ou ponts axiomatiques — pour atteindre un raisonnement conjoint correct à travers des domaines hétérogènes tout en tenant compte de la décidabilité et des garanties des solveurs.