Kaminski, Mark and Schneider, Sigurd and Smolka, Gert - 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
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies

Authors: Kaminski, Mark and Schneider, Sigurd and Smolka, Gert

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.


Source : oai:arXiv.org:1012.0746
DOI : 10.2168/LMCS-7(1:5)2011
Volume: Volume 7, Issue 1
Published on: March 21, 2011
Submitted on: May 14, 2010
Keywords: Computer Science - Logic in Computer Science,F.4.1, I.2.3, I.2.4


Share

Consultation statistics

This page has been seen 82 times.
This article's PDF has been downloaded 98 times.