Decision procedures for some strong hybrid logics
DOI:
https://doi.org/10.12775/LLP.2013.022Keywords
hybrid logics, modal logics, tableau calculi, sequent calculi, decision procedures, automated reasoningAbstract
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.
References
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
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 662
Number of citations: 2
