Paper detail

Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics

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.