Modular Termination and Combinability for Superposition Modulo Counter Arithmetic

Christophe Ringeissen 1 Valerio Senni 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 (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Modularity is a highly desirable property in the development of satisfiability procedures. In this paper we are interested in using a dedicated superposition calculus to develop satisfiability procedures for (unions of) theories sharing counter arithmetic. In the first place, we are concerned with the termination of this calculus for theories representing data structures and their extensions. To this purpose, we prove a modularity result for termination which allows us to use our superposition calculus as a satisfiability procedure for combinations of data structures. In addition, we present a general combinability result that permits us to use our satisfiability procedures into a non-disjoint combination method a la Nelson-Oppen without loss of completeness. This latter result is useful whenever data structures are combined with theories for which superposition is not applicable, like theories of arithmetic.
Type de document :
Communication dans un congrès
Cesare Tinelli and Viorica Sofronie-Stokkermans. Frontiers of Combining Systems, 8th International Symposium, FroCoS'2011, Oct 2011, Saarbruecken, Germany. Springer, 6989, pp.211-226, 2011, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-24364-6_15〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00636589
Contributeur : Christophe Ringeissen <>
Soumis le : jeudi 27 octobre 2011 - 17:26:06
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral

Identifiants

Citation

Christophe Ringeissen, Valerio Senni. Modular Termination and Combinability for Superposition Modulo Counter Arithmetic. Cesare Tinelli and Viorica Sofronie-Stokkermans. Frontiers of Combining Systems, 8th International Symposium, FroCoS'2011, Oct 2011, Saarbruecken, Germany. Springer, 6989, pp.211-226, 2011, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-24364-6_15〉. 〈inria-00636589〉

Partager

Métriques

Consultations de la notice

170