Global Caching for Coalgebraic Description Logics

Rajeev Gore, Clemens Kupke, Dirk Pattinson, Lutz Schröder

In: Jürgen Giesl , Reiner Haehnle (Hrsg.). Proceeding of the 5th International Joint Conference on Automated Reasoning. International Joint Conference on Automated Reasoning (IJCAR-2010) 5th befindet sich FLoC 2010 July 16-19 Edinburgh United Kingdom Lecture Notes in Computer Science (LNCS) Springer 2010.


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 uses the (known) tableau rules for the underlying modal logics, and is based on 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.


Weitere Links

hyGlobalCaching.pdf (pdf, 217 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence