Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus

Andrzej Indrzejczak

Bulletin of the Section of Logic (2016)

  • Volume: 45, Issue: 2
  • ISSN: 0138-0680

Abstract

top
In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi (SC) for S5 the presented system does not introduce any extra devices. Thus it is a standard version of SC but with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form.

How to cite

top

Andrzej Indrzejczak. "Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus." Bulletin of the Section of Logic 45.2 (2016): null. <http://eudml.org/doc/295552>.

@article{AndrzejIndrzejczak2016,
abstract = {In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi (SC) for S5 the presented system does not introduce any extra devices. Thus it is a standard version of SC but with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form.},
author = {Andrzej Indrzejczak},
journal = {Bulletin of the Section of Logic},
keywords = {Modal logic S5; decidability; normal forms; sequent calculus},
language = {eng},
number = {2},
pages = {null},
title = {Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus},
url = {http://eudml.org/doc/295552},
volume = {45},
year = {2016},
}

TY - JOUR
AU - Andrzej Indrzejczak
TI - Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus
JO - Bulletin of the Section of Logic
PY - 2016
VL - 45
IS - 2
SP - null
AB - In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to some 1-degree formula, i.e. a modally-flat formula with modal functors having only boolean formulas in its scope. In contrast to many sequent calculi (SC) for S5 the presented system does not introduce any extra devices. Thus it is a standard version of SC but with some additional simple rewrite rules. The procedure combines the proces of saturation of sequents with reduction of their elements to some normal modal form.
LA - eng
KW - Modal logic S5; decidability; normal forms; sequent calculus
UR - http://eudml.org/doc/295552
ER -

References

top
  1. [1] A. Avron, A Constructive Analysis of RM, Journal of Symbolic Logic 52 (1987), pp. 939–951. 
  2. [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. [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. [4] N. D. Belnap, Display Logic, Journal of Philosophical Logic 11(1982), pp. 375–417. 
  5. [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. [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. [7] R. Carnap, Modalities nad quantification, Journal of Symbolic Logic 11 (1946), pp. 33–64. 
  8. [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. [9] M. Fitting, Proof Methods for Modal and Intuitionistic Logics, Reidel, Dordrecht 1983. 
  10. [10] M. Fitting, Simple propositional S5 tableau system, Annals of Pure and Applied Logic 96 (1999), pp. 101–115. 
  11. [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. [12] G. E. Hughes, M. J. Cresswell, A New Introduction to Modal Logic, Routledge, London 1996. 
  13. [13] A. Indrzejczak, Cut-free double sequent calculus for S5, Logic Journal of the IGPL 6 (1998), pp. 505–516. 
  14. [14] S. Kanger, Provability in Logic, Almqvist & Wiksell, Stockholm 1957. 
  15. [15] S. Kripke, Semantical Analysis of Modal Logic I, Zeitschrift f¨ur Mathematische Logik und Grundlegen der Mathematik 9 (1963), pp. 67–96. 
  16. [16] H. Kurokawa, Hypersequent Calculi for Modal Logics Extending S4, [in:] New Frontiers in Artificial Intelligence, Springer 2014, pp. 51–68. 
  17. [17] O. Lahav, From Frame Properties to Hypersequent Rules in Modal Logics, [in:] Proceedings of LICS, Springer 2013, pp. 408–417. 
  18. [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. [19] G. Mints, Cut-free calculi of the S5 type, Studies in Constructive Mathematics and Mathematical Logic II (1970), pp. 79–82. 
  20. [20] S. Negri, Proof Analysis in Modal Logic, Journal of Philosophical Logic 34 (2005), pp. 507–544. 
  21. [21] M. Ohnishi, K. Matsumoto, Gentzen Method in Modal Calculi I, Osaka Mathematical Journal 9 (1957), pp. 113–130. 
  22. [22] M. Ohnishi, K. Matsumoto, Gentzen Method in Modal Calculi II, Osaka Mathematical Journal 11 (1959), pp. 115–120. 
  23. [23] F. Poggiolesi, A Cut-free Simple Sequent Calculus for Modal Logic S5, Review of Symbolic Logic 1 (2008), pp. 3–15. 
  24. [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. [25] F. Poggiolesi, Gentzen Calculi for Modal Propositional Logic, Springer 2011. 
  26. [26] G. Pottinger, Uniform cut-free formulations of T, S4 and S5 (abstract), Journal of Symbolic Logic 48 (1983), p. 900. 
  27. [27] D. Prawitz, Natural Deduction, Almqvist and Wiksell, Stockholm 1965. 
  28. [28] G. Restall, Proofnets for S5: sequents and circuits for modal logic, [in:] Lecture Notes in Logic 28 (2007), pp. 151–172. 
  29. [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. [30] T. Skura, Refutation methods in propositional modal logics, Semper 2013. 
  31. [31] P. Stouppa, The design of modal proof theories: the case of S5, Master Thesis, Dresden 2004. 
  32. [32] P. Stouppa, A deep inference system for the modal logic S5, Studia Logica 85 (2007), pp. 199–214. 
  33. [33] M. Takano, Subformula Property as a substitute for Cut-Elimination in Modal Propositional Logics, Mathematica Japonica 37/6 (1992), pp. 1129–1145. 
  34. [34] M. Wajsberg, Ein erweiteter Klassenkalkül, Monatshefte f¨ur Mathematik unf Physik 40 (1933), pp. 113–126. 
  35. [35] H. Wansing, Displaying Modal Logics, Kluwer Academic Publishers, Dordrecht 1999. 
  36. [36] J. J. Zeman, Modal Logic, Oxford University Press, Oxford 1973. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.