Publication details

Saarland University Computer Science

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               


Login to edit


Legal notice, Privacy policy