Combination of Convex Theories: Modularity, Deduction Completeness, and Explanation

Duc-Khanh Tran 1 Christophe Ringeissen 1, * Silvio Ranise 1 Hélène Kirchner 2
* Auteur correspondant
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 (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Decision procedures are key components of theorem provers and constraint satisfaction systems. Their modular combination is of prime interest for building efficient systems, but their effective use is often limited by poor interface capabilities, when such procedures only provide a simple ``sat/unsat'' answer. In this paper, we develop a rule-based framework to design cooperation schemas between such procedures while maintaining modularity of their interfaces. First, we use the rule-based framework to specify and prove the correctness of classic combination schemas by Nelson-Oppen and Shostak. Second, we introduce the concept of deduction complete satisfiability procedures, we show how to build them for large classes of theories, then we provide a schema to modularly combine them. Third, we consider the problem of modularly constructing explanations for combinations by re-using available proof-producing procedures for the component theories.
Type de document :
Rapport
[Research Report] RR-6688, INRIA. 2008, pp.34
Liste complète des métadonnées

Littérature citée [41 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00331479
Contributeur : Christophe Ringeissen <>
Soumis le : jeudi 16 octobre 2008 - 18:40:55
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : mardi 9 octobre 2012 - 13:55:09

Fichier

RR-6688.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00331479, version 1

Citation

Duc-Khanh Tran, Christophe Ringeissen, Silvio Ranise, Hélène Kirchner. Combination of Convex Theories: Modularity, Deduction Completeness, and Explanation. [Research Report] RR-6688, INRIA. 2008, pp.34. 〈inria-00331479〉

Partager

Métriques

Consultations de la notice

286

Téléchargements de fichiers

330