Tinelli, Cesare
- Ringeissen, Christophe
Rapport de recherche de l'INRIA -
Lorraine ,
Equipe :
PROTHEO 63 pages - Avril 1998 - Document en anglais
Titre français : Unions de théories non-disjointes et combinaisons de procédures de
satisfaisabilité : premiers résultats
Abstract : In this paper we outline a theoretical framework for the combination of decision procedures for the satisfiability of constraints with respect to a constrainttheory. We describe a general combination method which, given a procedure that decides constraint satisfiability with respect to a constraint theory ${\cal T}_1$ and one that decides constraint satisfiability with respect to a constraint theory ${\cal T}_2$, is able to produce a procedure that (semi-)decides constraint satisfiability with respect to the union of ${\cal T}_1$ and ${\cal T}_2$. We also provide some model-theoretic conditions on the constraint language and the component constraint theories for the method to be sound and complete, with special emphasis on the case in which the signatures of ${\cal T}_1$ and ${\cal T}_2$ are non-disjoint.
Résumé : Nous présentons dans cet article un cadre formel pour la combinaison des procédures de satisfaisabilité de contraintes par rapport à une théorie contrainte. Nous décrivons une méthode de combinaison générale qui, étant données une procédure de satisfaisabilité pour une théorie ${\cal T}_1$ et une autre pour une théorie ${\cal T}_2$, est capable de produire une procédure de (semi-)decision pour l'union de ${\cal T}_1$ et ${\cal T}_2$. On suit une approche fondée sur la théorie des modèles pour fournir également des conditions assurant la correction et la complétude de la méthode, en particulier lorsque les signatures de ${\cal T}_1$ et ${\cal T}_2$ sont non-disjointes.Nous présentons dans cet article un cadre formel pour la combinaison des procédures de satisfaisabilité de contraintes par rapport à une théorie contrainte. Nous décrivons une méthode de combinaison générale qui, étant données une procédure de satisfaisabilité pour une théorie ${\cal T}_1$ et une autre pour une théorie ${\cal T}_2$, est capable de produire une procédure de (semi-)decision pour l'union de ${\cal T}_1$ et ${\cal T}_2$. On suit une approche fondée sur la théorie des modèles pour fournir également des conditions assurant la correction et la complétude de la méthode, en particulier lorsque les signatures de ${\cal T}_1$ et ${\cal T}_2$ sont non-disjointes.
Key-Words : COMBINATION OF SATISFIABILITY PROCEDURES / DECISION PROBLEMS / CONSTRAINT-BASED
REASONING / AUTOMATED DEDUCTION
Mots-clés : COMBINAISON DE PROCÉDURES DE SATISFAISABILITÉ / PROBLÈMES DE DÉCISION /
RAISONNEMENT AVEC CONTRAINTES / DÉDUCTION AUTOMATIQUE
