This paper proposes a natural deduction system CNDS4 for classical S4 modal logic with necessity and possibility modalities. This new system is an extension of Parigot's Classical Natural Deduction with dual-context to formulate S4 modal logic. The modal λμ-calculus is also introduced as a computational extraction of CNDS4. It is an extension of both the λμ-calculus and the modal λ-calculus. Subject reduction, confluency, and strong normalization of the modal λμ-calculus are shown. Finally, the computational interpretation of the modal λμ-calculus, especially the computational meaning of the modal possibility operator, is discussed. © 2009 Springer-Verlag.
CITATION STYLE
Kimura, D., & Kakutani, Y. (2009). Classical natural deduction for S4 modal logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5904 LNCS, pp. 243–258). https://doi.org/10.1007/978-3-642-10672-9_18
Mendeley helps you to discover research relevant for your work.