Global Caching for Coalgebraic Description Logics (bibtex)
by Rajeev Gore, Clemens Kupke, Dirk Pattinson, 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:
Global Caching for Coalgebraic Description Logics (Rajeev Gore, Clemens Kupke, Dirk Pattinson, Lutz Schröder), In International Joint Conference on Automated Reasoning, IJCAR 2010 (Jürgen Giesl, Reiner Haehnle, eds.), 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.},
}
Powered by bibtexbrowser