Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies

Mark Kaminski, Sigurd Schneider, Gert Smolka

TABLEAUX 2009, Vol. 5607 of LNCS (LNAI), pp. 235-249, Springer, July 2009

We present a terminating tableau calculus for graded hybrid logic with global modalities, reflexivity, transitivity and role hierarchies. Termination of the system is achieved through pattern-based blocking. Previous approaches to related logics all rely on chain-based blocking. Besides being conceptually simple and suitable for efficient implementation, the pattern-based approach gives us a NExpTime complexity bound for the decision procedure.

DOI: 10.1007/978-3-642-02716-1_18

Download PDF        Show BibTeX               

@INPROCEEDINGS{KaminskiSchneiderSmolkaGraded,
  title = {Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies},
  author = {Mark Kaminski and Sigurd Schneider and Gert Smolka},
  year = {2009},
  month = {Jul},
  editor = {Martin Giese and Arild Waaler},
  publisher = {Springer},
  booktitle = {TABLEAUX 2009},
  series = {LNCS (LNAI)},
  volume = {5607},
  pages = {235-249},
}

Login to edit