Combining Proof-Producing Decision Procedures

Silvio Ranise 1 Christophe Ringeissen 1 Duc-Khanh Tran 1
1 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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Constraint solvers are key modules in many systems with reasoning capabilities (e.g., automated theorem provers). To incorporate constraint solvers in such systems, the capability of producing conflict sets or explanations of their results is crucial. For expressiveness, constraints are usually built out in unions of theories and constraint solvers in such unions are obtained by modularly combining solvers for the component theories. In this paper, we consider the problem of modularly constructing conflict sets for a combined theory by re-using available proof-producing procedures for the component theories. The key idea of our solution to this problem is the concept of explanation graph, which is a labelled, acyclic and undirected graph capable of recording the entailment of some equalities. Explanation graphs allow us to record explanations computed by a proof-producing procedure and to refine the Nelson-Oppen combination method to modularly build conflict sets for disjoint unions of theories. We also study how the computed conflict sets relate to an appropriate notion of minimality.
Type de document :
Communication dans un congrès
Boris Konev and Frank Wolter. 6th International Symposium o Frontiers of Combining Systems - FroCoS 2007, Sep 2007, Liverpool, United Kingdom. Springer Berlin / Heidelberg, 4720, pp.237-251, 2007, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-540-74621-8_16〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00187425
Contributeur : Christophe Ringeissen <>
Soumis le : mercredi 14 novembre 2007 - 14:59:26
Dernière modification le : jeudi 15 février 2018 - 08:48:09

Lien texte intégral

Identifiants

Citation

Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran. Combining Proof-Producing Decision Procedures. Boris Konev and Frank Wolter. 6th International Symposium o Frontiers of Combining Systems - FroCoS 2007, Sep 2007, Liverpool, United Kingdom. Springer Berlin / Heidelberg, 4720, pp.237-251, 2007, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-540-74621-8_16〉. 〈inria-00187425〉

Partager

Métriques

Consultations de la notice

203