2013 | 22 | 4 | 389-409
Article title

Decision procedures for some strong hybrid logics

Title variants
Languages of publication
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.
Physical description
  • Department of Logic and Methodology of Sciences, University of Lódź, ul. Kopcińskiego 16/18, 90-232 Łódź, Poland
  • Department of Logic and Methodology of Sciences, University of Lódź, ul. Kopcińskiego 16/18, 90-232 Łódź, Poland
  • 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
Document Type
Publication order reference
YADDA identifier
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.