Gorin D, Schröder L (2014)
Publication Language: English
Publication Type: Conference contribution, Original article
Publication year: 2014
Pages Range: 254-273
Conference Proceedings Title: Advances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic,"
URI: http://www8.cs.fau.de/publications
Open Access Link: http://www.aiml.net/volumes/volume10/Gorin-Schroeder.pdf
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
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: Download