Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus
Bulletin of the Section of Logic (2016)
- Volume: 45, Issue: 2
- ISSN: 0138-0680
Access Full Article
topAbstract
topHow to cite
topReferences
top- [1] A. Avron, A Constructive Analysis of RM, Journal of Symbolic Logic 52 (1987), pp. 939–951.
- [2] A. Avron, The method of hypersequents in the proof theory of propositional non-classical logic, [in:] W. Hodges, M. Hyland, C. Steinhorn, and J. Strauss, editors, Logic: from Foundations to Applications, Oxford University Press, Oxford (1996), pp. 1–32.
- [3] K. Bednarska and A. Indrzejczak, Hypersequent calculi for S5 - the methods of cut elimination, Logic and Logical Philosophy 24/3 (2015), pp. 277–311.
- [4] N. D. Belnap, Display Logic, Journal of Philosophical Logic 11(1982), pp. 375–417.
- [5] T. Braüner, A cut-free Gentzen formulation of the modal logic S5, Logic Journal of the IGPL 8 (2000), pp. 629–643.
- [6] T. Brünnler, A cut-free Gentzen formulation of the modal logic S5, Logic Journal of the IGPL 8 (2000), pp. 629–643.
- [7] R. Carnap, Modalities nad quantification, Journal of Symbolic Logic 11 (1946), pp. 33–64.
- [8] L. Farinas del Cerro and A. Herzig, Modal Deduction with Applications in Epistemic and Temporal Logics, [in:] D. Gabbay et all. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol. IV, Clarendon Press, Oxford 1995, pp. 499–594.
- [9] M. Fitting, Proof Methods for Modal and Intuitionistic Logics, Reidel, Dordrecht 1983.
- [10] M. Fitting, Simple propositional S5 tableau system, Annals of Pure and Applied Logic 96 (1999), pp. 101–115.
- [11] R. Goré, Tableau Methods for Modal and Temporal Logics, [in:] M. D’Agostino et al. (eds.), Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht 1999, pp. 297–396.
- [12] G. E. Hughes, M. J. Cresswell, A New Introduction to Modal Logic, Routledge, London 1996.
- [13] A. Indrzejczak, Cut-free double sequent calculus for S5, Logic Journal of the IGPL 6 (1998), pp. 505–516.
- [14] S. Kanger, Provability in Logic, Almqvist & Wiksell, Stockholm 1957.
- [15] S. Kripke, Semantical Analysis of Modal Logic I, Zeitschrift f¨ur Mathematische Logik und Grundlegen der Mathematik 9 (1963), pp. 67–96.
- [16] H. Kurokawa, Hypersequent Calculi for Modal Logics Extending S4, [in:] New Frontiers in Artificial Intelligence, Springer 2014, pp. 51–68.
- [17] O. Lahav, From Frame Properties to Hypersequent Rules in Modal Logics, [in:] Proceedings of LICS, Springer 2013, pp. 408–417.
- [18] B. Lellmann, D. Pattinson, Correspondence between Modal Jilbert Axioms and Sequent Rules with an Application to S5, [in:] D. Galmiche, D. Larchey-Wendling (eds.), TABLEAUX 2013. LNCS, vol. 8132, Springer 2013, pp. 219–233.
- [19] G. Mints, Cut-free calculi of the S5 type, Studies in Constructive Mathematics and Mathematical Logic II (1970), pp. 79–82.
- [20] S. Negri, Proof Analysis in Modal Logic, Journal of Philosophical Logic 34 (2005), pp. 507–544.
- [21] M. Ohnishi, K. Matsumoto, Gentzen Method in Modal Calculi I, Osaka Mathematical Journal 9 (1957), pp. 113–130.
- [22] M. Ohnishi, K. Matsumoto, Gentzen Method in Modal Calculi II, Osaka Mathematical Journal 11 (1959), pp. 115–120.
- [23] F. Poggiolesi, A Cut-free Simple Sequent Calculus for Modal Logic S5, Review of Symbolic Logic 1 (2008), pp. 3–15.
- [24] F. Poggiolesi, Reflecting the semantic features of S5 at the syntactic level, [in:] New Essays in Logic and Philosophy of Science, M. D’Agostino, G. Giorell, F. Laudisa, T. Pievani, C. Singaglia (eds.), London College Publications, 2010, pp. 13–25.
- [25] F. Poggiolesi, Gentzen Calculi for Modal Propositional Logic, Springer 2011.
- [26] G. Pottinger, Uniform cut-free formulations of T, S4 and S5 (abstract), Journal of Symbolic Logic 48 (1983), p. 900.
- [27] D. Prawitz, Natural Deduction, Almqvist and Wiksell, Stockholm 1965.
- [28] G. Restall, Proofnets for S5: sequents and circuits for modal logic, [in:] Lecture Notes in Logic 28 (2007), pp. 151–172.
- [29] M. Sato, A Study of Kripke-type Models for Some Modal Logics by Gentzen’s Sequential Method, Publications of the Research Institute for Mathematical Sciences, Kyoto University 1977, 13, pp. 381–468.
- [30] T. Skura, Refutation methods in propositional modal logics, Semper 2013.
- [31] P. Stouppa, The design of modal proof theories: the case of S5, Master Thesis, Dresden 2004.
- [32] P. Stouppa, A deep inference system for the modal logic S5, Studia Logica 85 (2007), pp. 199–214.
- [33] M. Takano, Subformula Property as a substitute for Cut-Elimination in Modal Propositional Logics, Mathematica Japonica 37/6 (1992), pp. 1129–1145.
- [34] M. Wajsberg, Ein erweiteter Klassenkalkül, Monatshefte f¨ur Mathematik unf Physik 40 (1933), pp. 113–126.
- [35] H. Wansing, Displaying Modal Logics, Kluwer Academic Publishers, Dordrecht 1999.
- [36] J. J. Zeman, Modal Logic, Oxford University Press, Oxford 1973.