2013/12/10 by Marta Cialdea Mayer, Mayer, Marta Cialdea
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.1312.2894
arXiv admin note: text overlap with arXiv:1210.5734
arxiv created 2013/12/10 · openalex publication_date 2013/12/10 · arxiv updated 2013/12/11 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
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.