2012/10/21 by Marta Cialdea Mayer, M. Cialdea Mayer, Mayer, M. Cialdea · 1 citation
Computer Science · Mathematics · #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies #cs.LO #math.LO
paper · pdf · doi:10.48550/arxiv.1210.5734
This paper has been withdrawn by the author because it is superseded by a new one: A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies(extended version)
openalex publication_date 2012/10/21 · arxiv created 2013/12/10 · arxiv updated 2013/12/11 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28
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.