Label-Free Proof Systems for Intuitionistic Modal Logic IS5

  • Didier Galmiche
  • Yakoub Salhi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


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.


Modal Logic Decision Procedure Proof System Mutual Induction Intuitionistic Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    Bull, R.A.: A modal extension of intuitionistic logic. Notre Dame Journal of Formal Logic 6, 142–145 (1965)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Bull, R.A.: MIPC as the formalization of an intuitionistic concept of modality. Journal of Symbolic Logic 31, 609–616 (1966)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Chadha, R., Macedonio, D., Sassone, V.: A hybrid intuitionistic logic: Semantics and decidability. Journal of Logic and Computation 16(1), 27–59 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Davies, R., Pfenning, F.: A modal analysis of staged computation. Journal of ACM 48(3), 555–604 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    Font, J.M.: Modality and possibility in some intuitionistic modal logics. Notre Dame Journal of Formal Logic 27, 533–546 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    Ono, H.: On some intuitionistic modal logics. Publications of the Research Institute for Mathematical Science 13, 55–67 (1977)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Ono, H., Suzuki, N.: Relations between intuitionistic modal logics and intermediate predicate logics. Reports on Mathematical Logic 22, 65–87 (1988)MathSciNetzbMATHGoogle Scholar
  13. 13.
    Prior, A.: Time and Modality. Clarendon Press, Oxford (1957)zbMATHGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Fischer Servi, G.: The finite model property for MIPQ and some consequences. Notre Dame Journal of Formal Logic XIX, 687–692 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Simpson, A.: The proof theory and semantics of intuitionistic modal logic. PhD thesis, University of Edinburgh (1994)Google Scholar
  17. 17.
    Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (1996)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Didier Galmiche
    • 1
  • Yakoub Salhi
    • 1
  1. 1.LORIA – UHP Nancy 1Vandœuvre-lès-NancyFrance

Personalised recommendations