The Complexity of Satisfiability for Fragments of Hybrid Logic -- Part I
Preprint
Abstract
The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments. In this paper, we investigate the effect of restricting the propositional part of the language on decidability and on the complexity of the satisfiability problem over arbitrary, transitive, total frames, and frames based on equivalence relations. We also consider different sets of modal and hybrid operators. We trace the border of decidability and give the precise complexity of most fragments, in particular for all fragments including negation. For the monotone fragments, we are able to distinguish the easy from the hard cases, depending on the allowed set of operators.Keywords
All Related Versions
- Version 1, 2009-06-08, ArXiv
- Published version: Journal of Applied Logic, 8 (4), 409.
This publication has 10 references indexed in Scilit:
- The Complexity of Poor Man's LogicJournal of Logic and Computation, 2001
- The computational complexity of hybrid temporal logicsLogic Journal of the IGPL, 2000
- Representation, reasoning, and relational structures: a hybrid logic manifestoLogic Journal of the IGPL, 2000
- Gap-languages and log-time complexity classesTheoretical Computer Science, 1997
- Counting Quantifiers, Successor Relations, and Logarithmic SpaceJournal of Computer and System Sciences, 1997
- Hierarchies of modal and temporal logics with reference pointersJournal of Logic, Language and Information, 1996
- The complexity of existential quantification in concept languagesArtificial Intelligence, 1992
- Satisfiability problems for propositional calculiTheory of Computing Systems, 1979
- The Computational Complexity of Provability in Systems of Modal Propositional LogicSIAM Journal on Computing, 1977
- The Two-Valued Iterative Systems of Mathematical Logic. (AM-5)1942