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.

    https://doi.org/10.2168/LMCS-7(1:5)2011
    Source: arXiv.org:1012.0746
    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
    Licence: arXiv.org - Non-exclusive license to distribute

    Classifications

    Mathematics Subject Classification 20201
    Sources:
    • [1] zbMATH Open.

    6 Documents citing this article

    Share and export

    Consultation statistics

    This page has been seen 2874 times.
    This article's PDF has been downloaded 645 times.