A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies (extended version)

TL;DR

This paper extends a tableau calculus for hybrid logic with binders to include transitivity and relation hierarchies, proving that their combination remains decidable, but adding graded modalities leads to undecidability without restrictions.

Contribution

It introduces a decision procedure for multi-modal hybrid logic with transitivity and relation hierarchies, demonstrating decidability of the combined features and analyzing the impact of graded modalities.

Findings

Decidability is maintained when combining transitivity and relation hierarchies.

Adding graded modalities without restrictions results in undecidability.

A sound, complete, and terminating calculus is constructed for the extended logic.

Abstract

In previous works, a tableau calculus has been defined, which constitutes a decision procedure for hybrid logic with the converse and global modalities and a restricted use of the binder. This work shows how to extend such a calculus to multi-modal logic enriched with features largely used in description logics: transitivity 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 does not endanger decidability. A further result proved in this work is that the logic extending the considered fragment with the addition of graded modalities (the modal counterpart of number restrictions of description logics) has an undecidable satisfiability problem, unless further syntactical restrictions are placed on the universal graded modality.