A comprehensive combination framework

Silvio Ghilardi 1 Enrica Nicolini 1 Daniele Zucchelli 1, 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 (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We define a general notion of a fragment within higher-order type theory; a procedure for constraint satisfiability in combined fragments is outlined, following Nelson-Oppen schema. The procedure is in general only sound, but it becomes terminating and complete when the shared fragment enjoys suitable noetherianity conditions and admits an abstract version of a "Keisler-Shelah-like" isomorphism theorem. We show that this general decidability transfer result covers recent work on combination in first-order theories as well as in various intensional logics such as description, modal, and temporal logics.
Type de document :
Article dans une revue
ACM Transactions on Computational Logic, Association for Computing Machinery, 2008, 9 (2), pp.Article n° 8. 〈10.1145/1342991.1342992〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00576602
Contributeur : Christophe Ringeissen <>
Soumis le : lundi 14 mars 2011 - 17:43:24
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Lien texte intégral

Identifiants

Citation

Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli. A comprehensive combination framework. ACM Transactions on Computational Logic, Association for Computing Machinery, 2008, 9 (2), pp.Article n° 8. 〈10.1145/1342991.1342992〉. 〈inria-00576602〉

Partager

Métriques

Consultations de la notice

98