Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics

Conference contribution
(Original article)


Publication Details

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
Language: English


Abstract


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

Gorin, Daniel Dr.
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Schröder, Lutz Prof. Dr.
Lehrstuhl für Informatik 8 (Theoretische Informatik)


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). Groningen, NL.

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.

BibTeX: 

Last updated on 2018-19-04 at 02:44