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

arXiv1210.5734MaRDI QIDQ6236535FDOQ6236535

Publication date: 21 October 2012

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.

This page was built for publication: Tableaux for multi-modal hybrid logic with binders, transitive relations and relation hierarchies

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6236535)