Sciweavers

TABLEAUX
2009
Springer

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

13 years 10 months ago
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies
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.
Mark Kaminski, Sigurd Schneider, Gert Smolka
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where TABLEAUX
Authors Mark Kaminski, Sigurd Schneider, Gert Smolka
Comments (0)