Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics
Abstract
While reasoning in a logic extending a complete Boolean basis is coNP-hard, restricting to conjunctive fragments of modal languages sometimes allows for tractable reasoning even in the presence of greatest fixpoints. One such example is the EL family of description logics; here, efficient reasoning is based on satisfaction checking in suitable small models that characterize formulas in terms of simulations. It is well-known, though, that not every conjunctive modal language has a tractable reasoning problem. Natural questions are then how common such tractable fragments are and how to identify them. In this work we provide sufficient conditions for tractability in a general way by considering unlabeled tableau rules for a given modal logic. We work in the framework of coalgebraic logic as a unifying semantic setting. Apart from recovering known results for description logics such as EL and FL0, we obtain new ones for conjunctive fragments of relational and non-relational modal logics with greatest fixpoints. Most notably we find tractable fragments of game logic and the alternating-time mu-calculus.
Cite
@article{arxiv.1401.6359,
title = {Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics},
author = {Daniel Gorín and Lutz Schröder},
journal= {arXiv preprint arXiv:1401.6359},
year = {2014}
}