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 allows an abstract version of a ‘Keisler-Shelah like’ isomorphism theorem.We show that this general decidability transfer result covers as special cases, besides applications which seem to be new, the recent extension of Nelson- Oppen procedure to non-disjoint signatures  and the fusion transfer of decidability of consistency of A-Boxes with respect to T-Boxes axioms in local abstract description systems ; in addition, it reduces decidability of modal and temporal monodic fragments  to their extensional and one-variable components.
|Titolo:||A Comprehensive Framework for Combining Decision Procedures|
|Parole Chiave:||Combination, fragments, decision procedures.|
|Settore Scientifico Disciplinare:||Settore M-FIL/02 - Logica e Filosofia della Scienza|
|Data di pubblicazione:||2005|
|Digital Object Identifier (DOI):||10.1007/11559306_1|
|Tipologia:||Book Part (author)|
|Appare nelle tipologie:||03 - Contributo in volume|