Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures

Cesare Tinelli Christophe Ringeissen 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper we outline a theoretical framework for the combination of decision procedures for constraint satisfiability. We describe a general combination method which, given a procedure that decides constraint satisfiability with respect to a constraint theory T1 and one that decides constraint satisfiability with respect to a constraint theory T2, produces a procedure that (semi-)decides constraint satisfiability with respect to the union of T1 and T2. We provide a number of 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 the component theories are non-disjoint. We also describe some general classes of theories to which our combination results apply, and relate our approach to some of the existing combination methods in the field.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2003, 290 (1), pp.291-353
Liste complète des métadonnées

https://hal.inria.fr/inria-00099668
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:39:57
Dernière modification le : jeudi 17 mai 2018 - 12:52:03

Identifiants

  • HAL Id : inria-00099668, version 1

Collections

Citation

Cesare Tinelli, Christophe Ringeissen. Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures. Theoretical Computer Science, Elsevier, 2003, 290 (1), pp.291-353. 〈inria-00099668〉

Partager

Métriques

Consultations de la notice

90