Sciweavers

Share
FROCOS
2005
Springer

A Comprehensive Framework for Combined Decision Procedures

9 years 5 months ago
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.
Silvio Ghilardi, Enrica Nicolini, Daniele Zucchell
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where FROCOS
Authors Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli
Comments (0)
books