Mark Kaminski ; Sigurd Schneider ; Gert Smolka - Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies

lmcs:969 - Logical Methods in Computer Science, March 21, 2011, Volume 7, Issue 1 - https://doi.org/10.2168/LMCS-7(1:5)2011
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role HierarchiesArticle

Authors: Mark Kaminski ; Sigurd Schneider ; Gert Smolka

    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.


    Volume: Volume 7, Issue 1
    Published on: March 21, 2011
    Imported on: May 14, 2010
    Keywords: Computer Science - Logic in Computer Science,F.4.1, I.2.3, I.2.4

    6 Documents citing this article

    Consultation statistics

    This page has been seen 1051 times.
    This article's PDF has been downloaded 456 times.