Logic and Logical Philosophy 22 (4):389-409 (2013)

Michał Zawidzki
University of Lodz
Hybrid logics are extensions of standard modal logics, which significantly increase the expressive power of the latter. Since most of hybrid logics are known to be decidable, decision procedures for them is a widely investigated field of research. So far, several tableau calculi for hybrid logics have been presented in the literature. In this paper we introduce a sound, complete and terminating tableau calculus T H(@,E,D, ♦ −) for hybrid logics with the satisfaction operators, the universal modality, the difference modality and the inverse modality as well as the corresponding sequent calculus S H(@,E,D, ♦ −) . They not only uniformly cover relatively wide range of various hybrid logics but they are also conceptually simple and enable effective search for a minimal model for a satisfiable formula. The main novelty is the exploitation of the unrestricted blocking mechanism introduced as an explicit, sound tableau rule
Keywords hybrid logics  tableau calculi  decision procedures  modal logics  automated reasoning  sequent calculi
Categories (categorize this paper)
DOI 10.12775/LLP.2013.022
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,231
Through your library

References found in this work BETA

Terminating Tableau Systems for Hybrid Logic with Difference and Converse.Mark Kaminski & Gert Smolka - 2009 - Journal of Logic, Language and Information 18 (4):437-464.
Lightweight Hybrid Tableaux.Guillaume Hoffmann - 2010 - Journal of Applied Logic 8 (4):397-408.
Nominal Substitution at Work with the Global and Converse Modalities.Serenella Cerrito & Marta Cialdea Mayer - 2010 - In Lev Beklemishev, Valentin Goranko & Valentin Shehtman (eds.), Advances in Modal Logic, Volume 8. CSLI Publications. pp. 59-76.

Add more references

Citations of this work BETA

Simple Cut Elimination Proof for Hybrid Logic.Andrezj Indrzejczak - 2016 - Logic and Logical Philosophy 25 (2):129-141.

Add more citations

Similar books and articles


Added to PP index

Total views
12 ( #812,474 of 2,518,158 )

Recent downloads (6 months)
1 ( #408,577 of 2,518,158 )

How can I increase my downloads?


My notes