Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics - Gorin, Daniel; Schröder, Lutz (Advances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic,", 2014)
While reasoning in a logic extending a complete Boolean basis is coNP-hard, re- stricting 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, eficient 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 suficient conditions for tractability in a general way by considering unlabeled tableau rules for a given modal logic. We work in the framework of coalgebraic modal logics as unifying semantic setting. Apart from recovering known results for description logics such as and 0, 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 μ-calculus.
UnivIS-Import:2015-03-09:Pub.2014.tech.IMMD.profes_1.subsum
Keywords: Convexity; Fixpoints; Materializers; Tractable reasoning