Decision procedures for some strong hybrid logics

Andrzej Indrzejczak, Michał Zawidzki



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 TH(@,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 SH(@,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.


hybrid logics; modal logics; tableau calculi; sequent calculi; decision procedures; automated reasoning

Full Text:



D’Agostino, M., “Tableau methods for Classical Propositional Logic”, pages 45–123 in: M. D’Agostino et al (eds.), Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht, 1999. DOI: 10.1007/978-94-017-1754-0_2

Areces, C., P. Blackburn, and M. Marx, “A road-map on complexity for hybrid logics”, pages 307–321 in: Proc. of the 8th Annual Conference of the European Association for Computer Science Logic (CSL 1999), Madrid, Spain. DOI: 10.1007/3-540-48168-0_22

Blackburn, P., “Internalizing labelled deduction”, J. Log. Comput., 10 (2000), 1: 137–168. DOI: 10.1093/logcom/10.1.137

Blackburn, P., and T. Bolander, “Termination for Hybrid Tableaus”, J. Log. Comput. 17 (2007), 3: 517–554.

Blackburn, P., Y. Venema, and M. de Rijke, Modal Logics, Cambridge University Press, 2002.

Bolander T., and T. Braüner, “Tableau-based decision procedures for hybrid logic”, J. Log. Comput., 16 (2006): 737–763. DOI: 10.1093/logcom/exl008

Braüner, T., Hybrid Logic and its Proof-Theory, Springer, 2011.

Cerrito S., and M. Cialdea-Mayer, “An efficient approach to nominal equalities in hybrid logic tableaux”, JANCL, 20 (2010), 1–2: 39–61. DOI: 10.3166/jancl.20.39-61

Cerrito S., and M. Cialdea-Mayer, “Nominal substitution at work with the global and converse modalities”, pages 59–76 in: AiML 2010, College Publications, 2010.

Demri, S., “A simple tableau system for the logic of elsewhere”, pages 177–192 in TABLEAUX-6, LNAI, Springer, 1996. DOI: 10.1007/3-540-61208-4_12

Fitting, M., “Modal proof theory”, pages pp. 85–138 in: P. Blackburn et al (eds.), Handbook of Modal Logic, Elsevier B.V., 2007. DOI: 10.1016/S1570-2464(07)80005-X

Götzmann, D., M. Kaminski, and G. Smolka, “Spartacus: A tableau prover for hybrid logic”, Electron. Notes Ther. Comput. Sci., 262 (2010): 127–139. DOI: 10.1016/j.entcs.2010.04.010

Hoffmann, G., “Lightweight hybrid tableaux”, J. of Applied Logic, 8 (2010): 397–408. DOI: 10.1016/j.jal.2010.08.003

Kaminski, M., and G. Smolka, “Terminating tableau systems for hybrid logic with difference and converse”, J. Log. Lang. Inf., 18 (2009): 437–464. DOI: 10.1007/s10849-009-9087-8

Cialdea-Mayer, M., and S. Cerrito, “Herod and pilate: two tableau provers for basic hybrid logic. System Description”, pages 255–262in IJCAR 2010, LNCS, Springer, 2010. DOI: 10.1007/978-3-642-14203-1_22

Mundhenk, M., and T. Schneider, “Undecidability of multi-modal hybrid logics”, Electron. Notes Ther. Comput. Sci., 174 (2007): 29–43. DOI: 10.1016/j.entcs.2006.11.024

Myers, R.S.R., and D. Pattinson, “Hybrid logic with the difference modality for generalizations of graphs”, J. of Applied Logic, 8 (2010): 441–458. DOI: 10.1016/j.jal.2010.08.011

Negri S., and J. von Plato, Structural Proof Theory, Cambridge, 2001.

Schmidt, R.A., and D. Tishkovsky, “Automated synthesis of tableau calculi”, Log. Meth. Comput. Sci., 7 (2011), 2: 1–32. DOI: 10.2168/LMCS-7(2:6)2011

Schmidt R.A., and D. Tishkovsky, “Using tableau to decide description logics with full role negation and identity”, 2012. PDF

Tzakova, M., “Tableau calculi for hybrid logics”, LNCS, 1617 (1999): 278–292. DOI: 10.1007/3-540-48754-9_24

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism