Talk "Universal Simulands and Subsumption Checking in Lightweight Coalgebraic Logics"

by Lutz Schröder

Wed, 08 January 2014 at 10:00 am in Theddingworth near Leicester, UK

Joint work with: Daniel Gorin

Abstract: While reasoning in logics extending a Boolean propositional base is necessarily at least coNP-hard, some families of specifically designed light-weight logics allow for tractable, i.e.\ polynomial-time reasoning, and hence may be expected to scale to large reasoning problems. One example of this type is the EL family of description logics; in this case, efficient reasoning may be based on simulation checking between suitable small models. In the current work, we lift this principle to the level of generality of coalgebraic logic. We thus not only identify tractable fragments of non-relational logics whose semantics features, e.g., neighbourhoods or integer weights, but we also obtain new insights in the standard relational setting, e.g. on polynomial-time reasoning with global assumptions in modal logics featuring only box and conjunction.