Tableaux for multi-modal hybrid logic with binders, transitive relations and relation hierarchies

TL;DR

This paper extends a tableau calculus for hybrid logic to include multi-modal features with transitive relations and relation hierarchies, proving the combined logic remains decidable.

Contribution

It introduces a tableau calculus for multi-modal hybrid logic with transitive relations and hierarchies, establishing its decidability.

Findings

The calculus is sound, complete, and terminating.

Decidability is preserved with combined features.

Extends previous hybrid logic decision procedures.

Abstract

In a previous paper, a tableau calculus has been presented, which constitute a decision procedure for hybrid logic with the converse and global modalities and a restricted use of the binder. This work extends such a calculus to multi-modal logic with transitive relations and relation inclusion assertions. The separate addition of either transitive relations or relation hierarchies to the considered decidable fragment of multi-modal hybrid logic can easily be shown to stay decidable, by resorting to results already proved in the literature. However, such results do not directly allow for concluding whether the logic including both features is still decidable. The existence of a terminating, sound and complete calculus for the considered logic proves that the addition of transitive relations and relation hierarchies to such an expressive decidable fragment of hybrid logic yields a decidable logic.