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

TL;DR

This paper introduces a new terminating tableau calculus for graded hybrid logic with global modalities, role hierarchies, and transitivity, using pattern-based blocking to ensure efficiency and complexity bounds.

Contribution

It proposes a novel pattern-based blocking method for tableau calculus, improving simplicity and efficiency over previous chain-based approaches.

Findings

Achieves NExpTime complexity bound for the decision procedure.

Ensures termination through pattern-based blocking.

Conceptually simple and suitable for implementation.

Abstract

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.