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. Ghilardi
Primo
;
E. Nicolini
Secondo
;
D. Zucchelli
Ultimo
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.
Combination; Decision procedures; Higher-order logic; Modal and description logics; Satisfiability modulo theory
Settore M-FIL/02 - Logica e Filosofia della Scienza
mar-2008
http://www.acm.org/pubs/tocl/accepted/290zucchelli.pdf
Article (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/53427
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 17
  • ???jsp.display-item.citation.isi??? 16
social impact