A Comprehensive Framework for Combined Decision Procedures

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 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 NelsonOppen procedure to non-disjoint signatures [16] and the fusion transfer of decidability of consistency of A-Boxes with respect to T-Boxes axioms in local abstract description systems [9]; in addition, it reduces decidability of modal and temporal monodic fragments [32] to their extensional and one-variable components.

• Type: Conference
• Year: 2005
• Where: FROCOS
• Authors: Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli
• Keywords: FROCOS 2005, General Decidability Transfer, Suitable Noetherianity Conditions, Temporal Monodic Fragments