Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics
Author(s): Gorin D, Schröder L
Publication year: 2014
Conference Proceedings Title: Advances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic,"
Pages range: 254-273
Event: Advances in Modal Logic
Event location: Groningen
Start date of the event: 05/08/2014
End date of the event: 08/08/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.
FAU Authors / FAU Editors How to cite
APA: Gorin, D., & Schröder, L. (2014). Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics. In Advances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic," (pp. 254-273).
MLA: Gorin, Daniel, and Lutz Schröder. "Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics." Proceedings of the Advances in Modal Logic, Groningen 2014. 254-273.