Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics

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,"

Event location: Groningen

URI: http://www8.cs.fau.de/publications

Open Access Link: http://www.aiml.net/volumes/volume10/Gorin-Schroeder.pdf

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.

Authors with CRIS profile

Daniel Gorin Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik)

Related research project(s)

Probabilistische Beschreibungslogik als Fragment der Probabilistischen Logik Erster Stufe (ProbDL) April 1, 2011 - April 1, 2014

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: Download