Abstract
In this paper we propose proof systems without labels for the intuitionistic modal logic IS5 that are based on a new multi-contextual sequent structure appropriate to deal with such a logic. We first give a label-free natural deduction system and thus derive natural deduction systems for the classical modal logic S5 and also for an intermediate logic IM5. Then we define a label-free sequent calculus for IS5 and prove its soundness and completeness. The study of this calculus leads to a decision procedure for IS5 and thus to an alternative syntactic proof of its decidability.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: Hodges, W., Hyland, M., Steinhorn, C., Truss, J. (eds.) Logic: From Foundations to Applications, pp. 1–32. Oxford University Press, Oxford (1996)
Bezhanishvili, G., Zakharyaschev, M.: Logics over MIPC. In: Proceedings of Sequent Calculi and Kripke Semantics for Non-Classical Logics, pp. 86–95. Kyoto University (1997)
Bull, R.A.: A modal extension of intuitionistic logic. Notre Dame Journal of Formal Logic 6, 142–145 (1965)
Bull, R.A.: MIPC as the formalization of an intuitionistic concept of modality. Journal of Symbolic Logic 31, 609–616 (1966)
Chadha, R., Macedonio, D., Sassone, V.: A hybrid intuitionistic logic: Semantics and decidability. Journal of Logic and Computation 16(1), 27–59 (2006)
Davies, R., Pfenning, F.: A modal analysis of staged computation. Journal of ACM 48(3), 555–604 (2001)
Fairtlough, M., Mendler, M.: An intuitionistic modal logic with applications to the formal verification of hardware. In: Kleine Büning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 354–368. Springer, Heidelberg (1996)
Font, J.M.: Modality and possibility in some intuitionistic modal logics. Notre Dame Journal of Formal Logic 27, 533–546 (1986)
Jia, L., Walker, D.: Modal proofs as distributed programs (extended abstract). In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 219–233. Springer, Heidelberg (2004)
Murphy VII, T., Crary, K., Harper, R., Pfenning, F.: A symmetric modal lambda calculus for distributed computing. In: Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS), pp. 286–295. IEEE Press, Los Alamitos (2004)
Ono, H.: On some intuitionistic modal logics. Publications of the Research Institute for Mathematical Science 13, 55–67 (1977)
Ono, H., Suzuki, N.: Relations between intuitionistic modal logics and intermediate predicate logics. Reports on Mathematical Logic 22, 65–87 (1988)
Prior, A.: Time and Modality. Clarendon Press, Oxford (1957)
Restall, G.: Proofnets for S5: sequents and circuits for modal logic. In: Dimitracopoulos, C., Newelski, L., Normann, D. (eds.) Logic Colloquium 2005. Lecture Notes in Logic, vol. 28, pp. 151–172. Cambridge University Press, Cambridge (2007)
Fischer Servi, G.: The finite model property for MIPQ and some consequences. Notre Dame Journal of Formal Logic XIX, 687–692 (1978)
Simpson, A.: The proof theory and semantics of intuitionistic modal logic. PhD thesis, University of Edinburgh (1994)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Galmiche, D., Salhi, Y. (2010). Label-Free Proof Systems for Intuitionistic Modal Logic IS5 . In: Clarke, E.M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science(), vol 6355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17511-4_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-17511-4_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17510-7
Online ISBN: 978-3-642-17511-4
eBook Packages: Computer ScienceComputer Science (R0)