Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts
| dc.contributor.author | Braüner, Torben | |
| dc.date.accessioned | 2022-08-25T13:00:35Z | |
| dc.date.available | 2022-08-25T13:00:35Z | |
| dc.date.issued | 2022-01-07 | |
| dc.identifier.issn | 0138-0680 | |
| dc.identifier.uri | http://hdl.handle.net/11089/42921 | |
| dc.description.abstract | This paper is about non-labelled proof-systems for hybrid logic, that is, proofsystems where arbitrary formulas can occur, not just satisfaction statements. We give an overview of such proof-systems, focusing on analytic systems: Natural deduction systems, Gentzen sequent systems and tableau systems. We point out major results and we discuss a couple of striking facts, in particular that nonlabelled hybrid-logical natural deduction systems are analytic, but this is not proved in the usual way via step-by-step normalization of derivations. | en |
| dc.language.iso | en | |
| dc.publisher | Wydawnictwo Uniwersytetu Łódzkiego | pl |
| dc.relation.ispartofseries | Bulletin of the Section of Logic;2 | en |
| dc.rights.uri | https://creativecommons.org/licenses/by-nc-nd/4.0 | |
| dc.subject | hybrid logic | en |
| dc.subject | natural deduction systems | en |
| dc.subject | sequent systems | en |
| dc.subject | normalization | en |
| dc.subject | cut-elimination | en |
| dc.subject | analycity | en |
| dc.title | Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts | en |
| dc.type | Other | |
| dc.page.number | 143-162 | |
| dc.contributor.authorAffiliation | Roskilde University, Department of People and Technology, Building 10.1, Universitetsvej 1, P.O. Box 260, DK-4000 Roskilde, Denmark | en |
| dc.identifier.eissn | 2449-836X | |
| dc.references | M. Baaz, A. Leitsch, Methods of Cut-Elimination, vol. 34 of Trends in Logic Series, Springer, Dordrecht (2011), DOI: https://doi.org/10.1007/978-94-007-0320-9 | en |
| dc.references | G. Bierman, V. de Paiva, On an Intuitionistic Modal Logic, Studia Logica, vol. 65 (2000), pp. 383–416, DOI: https://doi.org/10.1023/A:1005291931660 | en |
| dc.references | P. Blackburn, T. Bolander, T. Braüner, K. Jørgensen, Completeness and Termination for a Seligman-style Tableau System, Journal of Logic and Computation, vol. 27(1) (2017), pp. 81–107, DOI: https://doi.org/10.1093/logcom/exv052 | en |
| dc.references | T. Braüner, Two Natural Deduction Systems for Hybrid Logic: A Comparison, Journal of Logic, Language and Information, vol. 13 (2004), pp. 1–23, DOI: https://doi.org/10.1023/A:1026187215321 | en |
| dc.references | T. Braüner, Hybrid Logic, [in:] E. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Stanford University (2005), URL: http://plato.stanford.edu/entries/logic-hybrid, substantive revision in 2017. | en |
| dc.references | T. Braüner, Hybrid Logic and its Proof-Theory, vol. 37 of Applied Logic Series, Springer, Dordrecht (2011), DOI: https://doi.org/10.1007/978-94-007-0002-4 | en |
| dc.references | T. Braüner, Hybrid-Logical Reasoning in the Smarties and Sally-Anne Tasks, Journal of Logic, Language and Information, vol. 23 (2014), pp. 415–439, DOI: https://doi.org/10.1007/s10849-014-9206-z | en |
| dc.references | T. Braüner, I. Polyanskaya, P. Blackburn, A logical investigation of false-belief tasks, [in:] Proceedings of the 40th Annual Meeting of the Cognitive Science Society, Cognitive Science Society, Madison, Wisconsin, USA (2018), pp. 45–46, URL: https://cogsci.mindmodeling.org/2018/papers/0023/0023.pdf | en |
| dc.references | M. Fitting, Modal Proof Theory, [in:] P. Blackburn, J. van Benthem, F. Wolter (eds.), Handbook of Modal Logic, vol. 3 of Studies in Logic and Practical Reasoning, Elsevier, Amsterdam (2007), pp. 85–138, DOI: https://doi.org/10.1016/S1570-2464(07)80005-X | en |
| dc.references | A. From, Synthetic Completeness for a Terminating Seligman-Style Tableau System, [in:] U. de’Liguoro, S. Berardi, T. Altenkirch (eds.), 26th International Conference on Types for Proofs and Programs (TYPES 2020), vol. 188 of Leibniz International Proceedings in Informatics (LIPIcs), Leibniz-Zentrum für Informatik, Schloss Dagstuhl (2021), pp. 5:1–5:17, DOI: https://doi.org/10.4230/LIPIcs.TYPES.2020.5 | en |
| dc.references | A. From, P. Blackburn, J. Villadsen, Formalizing a Seligman-Style Tableau System for Hybrid Logic, [in:] N. Peltier, V. Sofronie-Stokkermans (eds.), Proceedings of 10th International Joint Conference on Automated Reasoning (IJCAR), vol. 12166 of Lecture Notes in Computer Science, Springer-Verlag, Cham (2020), pp. 474–482, DOI: https://doi.org/10.1007/978-3-030-51074-9_27 | en |
| dc.references | J.-Y. Girard, Linear Logic, Theoretical Computer Science, vol. 50(1) (1987), pp. 1–102, DOI: https://doi.org/10.1016/0304-3975(87)90045-4 | en |
| dc.references | J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, vol. 7 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge (1989). | en |
| dc.references | A. Indrzejczak, Natural Deduction, Hybrid Systems and Modal Logics, vol. 30 of Trends in Logic Series, Springer, Dordrecht (2010), DOI: https://doi.org/10.1007/978-90-481-8785-0 | en |
| dc.references | K. Jørgensen, P. Blackburn, T. Bolander, T. Braüner, Completeness Proofs for Seligman-style Tableau Systems, [in:] L. Beklemishev, S. Demri (eds.), Proceedings of Advances in Modal Logic 2016, vol. 11 of Advances in Modal Logic, College Publications, Rickmansworth (2016), pp. 302–321, DOI: https://doi.org/10.1007/978-3-030-51074-9_27 | en |
| dc.references | H. Kushida, M. Okada, A Proof-Theoretic Study of the Correspondence of Hybrid Logic and Classical Logic, Journal of Logic, Language and Information, vol. 16 (2007), pp. 35–61, DOI: https://doi.org/10.1007/s10849-006-9023-0 | en |
| dc.references | D. Prawitz, Natural Deduction. A Proof-Theoretical Study, Almqvist and Wiksell, Stockholm (1965). | en |
| dc.references | D. Prawitz, Proofs and the Meaning and Completeness of the Logical Constants, [in:] J. Hintikka, I. Niiniluoto, E. Saarinen (eds.), Essays on Mathematical and Philosophical Logic, vol. 122 of Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science), Springer, Dordrecht (1979), pp. 25–40, DOI: https://doi.org/10.1007/978-94-009-9825-4_2 | en |
| dc.references | L. Rips, Logical Approaches to Human Deductive Reasoning, [in:] J. Adler, L. Rips (eds.), Reasoning: Studies of Human Inference and Its Foundations, Cambridge University Press, Cambridge (2008), pp. 187–205. | en |
| dc.references | J. Seligman, The Logic of Correct Description, [in:] M. de Rijke (ed.), Advances in Intensional Logic, vol. 7 of Applied Logic Series, Springer, Dordrecht (1997), pp. 107 – 135, DOI: https://doi.org/10.1007/978-94-015-8879-9_5 | en |
| dc.references | J. Seligman, Internalization: The Case of Hybrid Logics, Journal of Logic and Computation, vol. 11(5) (2001), pp. 671–689, DOI: https://doi.org/10.1093/logcom/11.5.671 | en |
| dc.references | A. Simpson, The Proof Theory and Semantics of Intuitionistic Modal logic, Ph.D. thesis, University of Edinburgh (1994). | en |
| dc.references | H. Wansing, Sequent Systems for Modal Logics, [in:] D. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic, 2nd ed., vol. 8, Springer, Dordrecht (2002), pp. 61–145, DOI: https://doi.org/10.1007/978-94-010-0387-2_2 | en |
| dc.contributor.authorEmail | torben@ruc.dk | |
| dc.identifier.doi | 10.18778/0138-0680.2022.02 | |
| dc.relation.volume | 51 |
Pliki tej pozycji
Pozycja umieszczona jest w następujących kolekcjach
Poza zaznaczonymi wyjątkami, licencja tej pozycji opisana jest jako https://creativecommons.org/licenses/by-nc-nd/4.0