by Rajeev Gore, Clemens Kupke, Dirk Pattinson and Lutz Schröder
Abstract:
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.
Reference:
Rajeev Gore, Clemens Kupke, Dirk Pattinson and Lutz Schröder: Global Caching for Coalgebraic Description Logics, In Jürgen Giesl, Reiner Haehnle, eds.: International Joint Conference on Automated Reasoning, IJCAR 2010, Lecture Notes in Computer Science, vol. 6173, pp. 46–60, Springer, 2010. [preprint]
Bibtex Entry:
@InProceedings{GoreEA10,
author = {Rajeev Gore and Clemens Kupke and Dirk Pattinson and Lutz Schr{\"o}der},
title = {Global Caching for Coalgebraic Description Logics},
year = {2010},
editor = {J{\"u}rgen Giesl and Reiner Haehnle},
booktitle = {International Joint Conference on Automated Reasoning, IJCAR 2010},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6173},
pages = {46-60},
keywords = {Coalgebra description logic modal logic hybrid logic tableaux global caching},
comment = { <a href = "http://www8.informatik.uni-erlangen.de/~schroeder/papers/hyGlobalCaching.pdf"> [preprint] </a>},
abstract = { 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.},
}