A Gentle Non-Disjoint Combination of Satisfiability Procedures

Paula Chocron 1, 2 Pascal Fontaine 3 Christophe Ringeissen 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : A satisfiability problem is often expressed in a combination of theories, and a natural approach consists in solving the problem by combining the satisfiability procedures available for the component theories. This is the purpose of the combination method introduced by Nelson and Oppen. However, in its initial presentation, the Nelson-Oppen combination method requires the theories to be signature-disjoint and stably infinite (to guarantee the existence of an infinite model). The notion of gentle theory has been introduced in the last few years as one solution to go beyond the restriction of stable infiniteness, but in the case of disjoint theories. In this paper, we adapt the notion of gentle theory to the non-disjoint combination of theories sharing only unary predicates (plus constants and the equality). Like in the disjoint case, combining two theories, one of them being gentle, requires some minor assumptions on the other one. We show that major classes of theories, i.e.\ Loewenheim and Bernays-Schoenfinkel-Ramsey, satisfy the appropriate notion of gentleness introduced for this particular non-disjoint combination framework.
Type de document :
Communication dans un congrès
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Jul 2014, Vienna, Austria. Springer, 8562, pp.122-136, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08587-6_9〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01087162
Contributeur : Christophe Ringeissen <>
Soumis le : mardi 25 novembre 2014 - 15:04:08
Dernière modification le : jeudi 22 septembre 2016 - 14:31:59

Identifiants

Citation

Paula Chocron, Pascal Fontaine, Christophe Ringeissen. A Gentle Non-Disjoint Combination of Satisfiability Procedures. Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Jul 2014, Vienna, Austria. Springer, 8562, pp.122-136, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08587-6_9〉. 〈hal-01087162〉

Partager

Métriques

Consultations de la notice

155