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 documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.