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

Logical Methods in Computer Science 7(1:5), March 2011

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.

Available at the LMCS web page or at arXiv (arXiv:1012.0746).

Show BibTeX               

@ARTICLE{KaminskiEtAl:2011:TableauxGHL,
  title = {Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies},
  author = {Mark Kaminski and Sigurd Schneider and Gert Smolka},
  year = {2011},
  month = {Mar},
  journal = {Logical Methods in Computer Science},
  volume = {7},
  number = {1:5},
}

Login to edit