Simple cut elimination proof for hybrid logic
DOI:
https://doi.org/10.12775/LLP.2016.004Keywords
hybrid logic, cut elimination theorem, hypersequent calculi, sequent calculi, geometric conditionsAbstract
In the paper we present a relatively simple proof of cut elimination theorem for variety of hybrid logics in the language with satisfaction operators and universal modality. The proof is based on the strategy introduced originally in the framework of hypersequent calculi but it works well also for standard sequent calculi. Sequent calculus examined in the paper works on so called satisfaction formulae and cover all logics adequate with respect to classes of frames defined by so called geometric conditions.References
Blackburn, P., “Nominal tense logic”, Notre Dame Journal of Formal Logic, 34, 1 (1992): 56–83. DOI:10.1305/ndjfl/1093634564
Blackburn, P., “Internalizing labelled deduction”, Journal of Logic and Computation, 10, 1 (2000): 137–168. DOI:10.1093/logcom/10.1.137
Bolander, T., and T. Braüner, “Tableau-based decision procedures for hybrid logic”, Journal of Logic and Computation, 16, 6 (2006): 737–763. DOI:10.1093/logcom/exl008
Braüner, T., “Natural deduction for hybrid logic”, Journal of Logic and Computation, 14, 3 (2004): 137–168. DOI:10.1093/logcom/14.3.329
Braüner, T., “Hybrid logic”, in Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Winter 2014 edition, 2014. http://plato.stanford.edu/archives/win2014/entries/logic-hybrid/
Braüner, T., Hybrid Logic and its Proof-Theory, Roskilde, 2009.
Ciabattoni, A., G. Metcalfe, and F. Montagna, “Algebraic and proof-theoretic characterizations of truth stressers for mtl and its extensions”, Fuzzy Sets and Systems, 161, 3 (2010): 369–389. DOI:10.1016/j.fss.2009.09.001
Curry, H.B., Foundations of Mathematical Logic, McGraw-Hill, New York, 1963.
Demri, S., “Sequent calculi for nominal tense logics: A step towards mechanization”, pages 140–154 in N. Murray (ed.), Tableaux 99, volume 1617 of Lecture Notes in Computer Science, Springer, Berlin, 1999.
Demri, S., and R. Goré, “Cut-free display calculi for nominal tense logics”, pages 155–170 in N. Murray (ed.), Tableaux 99, volume 1617 of Lecture Notes in Computer Science, Springer, Berlin, 1999.
Gargov, G., and V. Goranko, “Modal logic with names”, Journal of Philosophical Logic, 22, 6 (1993): 607–636. DOI:10.1007/BF01054038
Goranko, V., “Temporal logic with reference pointers”, chapter 9, pages 133–148, in Temporal Logic, volume 827 of Lecture Notes in Computer Science, Springer, 1994. DOI:10.1007/BFb0013985
Indrzejczak, A., “Modal hybrid logic”, Logic and Logical Philosophy, 16, 2–3 (2007): 147–257. DOI:10.12775/LLP.2007.006
Indrzejczak, A., Natural Deduction, Hybrid Systems and Modal Logics, vol. 30 of Trends in Logic, Springer, 2010. DOI:10.1007/978-90-481-8785-0
Indrzejczak, A., and M. Zawidzki, “Decision procedures for some strong hybrid logics”, Logic and Logical Philosophy, 22, 4 (2013): 389–409. DOI:10.12775/LLP.2013.022
Negri, S., “Proof analysis in modal logic”, Journal of Philosophical Logic, 34, 5–6 (2005): 507–544. DOI:10.1007/s10992-005-2267-3
Prior, A., Time and Modality, Oxford University Press, Oxford, 1957.
Seligman, J., “Internalization: The case of hybrid logics”, Journal of Logic and Computation, 11, 5 (2001): 671–689. DOI:10.1093/logcom/11.5.671
Zawidzki, M., Deductive Systems and the Decidability Problem for Hybrid Logics, Univ. of Lódź Press and Jagielonian Univ. Press, 2013.
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 74
Number of citations: 4
