Skip to Main content Skip to Navigation
Journal articles

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Journal articles
Complete list of metadata
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Monday, March 14, 2011 - 5:43:24 PM
Last modification on : Friday, January 21, 2022 - 3:08:56 AM



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⟩



Record views