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.
A comprehensive combination framework / S. Ghilardi, E. Nicolini, D. Zucchelli. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 9:2(2008 Mar), pp. 8.1-8.54.
A comprehensive combination framework
S. GhilardiPrimo
;E. NicoliniSecondo
;D. ZucchelliUltimo
2008
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.
Pubblicazioni consigliate
I metadati presenti in AIR sono rilasciati con licenza CCO mentre i file delle pubblicazioni sono rilasciati con licenza CC BY-SA, salvo diversa indicazione. In caso di violazione di copyright, contattare l'assistenza di AIR
