Global Caching for Coalgebraic Description Logics

Dirk Pattinson

(Imperial College)

Coalgebraic description logics offer a common semantic umbrella for extensions of description logics with reasoning principles outside relational semantics, e.g. quantitative uncertainty, non-monotonic conditionals, or coalitional power. Specifically, we work in coalgebraic logic with global assumptions (i.e. a general TBox), nominals, and satisfaction operators, and prove soundness and completeness of an associated tableau algorithm of optimal complexity EXPTIME. The algorithm is based on global caching, which raises hopes of practically feasible implementation. Instantiation of this result to concrete logics yields new algorithms in all cases including standard relational hybrid logic.

In the talk, I will introduce the logics and the reasoning systems in a light-weight way by means of a running example, which will help to highlight the crucial features of the new algorithms.

This is joint work with Rajeev Gore (ANU), Clemens Kupke (Imperial) and Lutz Schroeder (DFKI Bremen).
Thursday 27th May 2010, 14:00
Video Conferencing Room - Far-134
Department of Computer Science