Terminating Tableaux for Graded Hybrid Logic with Global Modalities and
Role HierarchiesArticle
Authors: Mark Kaminski ; Sigurd Schneider ; Gert Smolka
NULL##NULL##NULL
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.
Yaroslav Petrukhin;Michał Zawidzki, Lecture notes in computer science, From Simplified Kripke-Style Semantics to Simplified Analytic Tableaux for Some Normal Modal Logics, pp. 116-131, 2019, 10.1007/978-3-030-35166-3_9.
Marta Cialdea Mayer, 2014, Extended Decision Procedure for a Fragment of HL with Binders, Journal of Automated Reasoning, 53, 3, pp. 305-315, 10.1007/s10817-014-9307-z.
Michał Zawidzki;Renate A. Schmidt;Dmitry Tishkovsky, 2012, Satisfiability problem for modal logic with global counting operators coded in binary is NExpTime-complete, Information Processing Letters, 113, 1-2, pp. 34-38, 10.1016/j.ipl.2012.09.007.