Machine-Checked Proof-Theory for Propositional Modal Logics

  • Jeremy E. Dawson
  • Rajeev GoréEmail author
  • Jesse Wu
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 28)


We describe how we machine-checked the admissibility of the standard structural rules of weakening, contraction and cut for multiset-based sequent calculi for the unimodal logics S4, S4.3 and K4De, as well as for the bimodal logic \(\mathrm {S4C}\) recently investigated by Mints. Our proofs for both S4 and S4.3 appear to be new while our proof for \(\mathrm {S4C}\) is different from that originally presented by Mints, and appears to avoid the complications he encountered. The paper is intended to be an overview of how to machine-check proof theory for readers with a good understanding of proof theory.



Jeremy E. Dawson—Supported by Australian Research Council Grant DP120101244.


  1. 1.
    N.D. Belnap, Display logic. J. Philos. Logic 11(4), 375–417 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    G. Bierman, V. de Paiva, Intuitionistic necessity revisited, in Proceedings of the Logic at Work Conference (1996)Google Scholar
  3. 3.
    C. Castellini, Automated reasoning in quantified modal and temporal logics. AI Commun. 19(2), 183–185 (2006)MathSciNetGoogle Scholar
  4. 4.
    J.M. Davoren, R. Goré, Bimodal logics for reasoning about continuous dynamics, in Advances in Modal Logic 3, papers from the Third Conference on “Advances in Modal Logic”, Leipzig (Germany), Oct 2000 (2000), pp. 91–111Google Scholar
  5. 5.
    J. Dawson, Mix-elimination for S4 (2014). Included in Isabelle code base
  6. 6.
    J.E. Dawson, R. Goré, Generic methods for formalising sequent calculi applied to provability logic, in Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’10 (Springer-Verlag, Berlin, Heidelberg, 2010), pp. 263–277Google Scholar
  7. 7.
    K. Dosen, P. Schroder-Heister (eds.), Substructural Logics. Studies in Logic and Computation, vol. 2 (Clarendon Press, 1993)Google Scholar
  8. 8.
    G. Gentzen, Untersuchungen über das logische schließen. Mathematische Zeitschrift 39, 176–210 and 405–431 (1935)Google Scholar
  9. 9.
    J.-Y. Girard, Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    M.J.C. Gordon, T.F. Melham (eds.), Introduction to HOL: A Theorem-proving Environment for Higher-Order Logic (Cambridge University Press, Cambridge, 1993)Google Scholar
  11. 11.
    R. Goré, R. Ramanayake, Valentini’s cut-elimination for provability logic resolved, in Advances in Modal Logic, vol. 7 (College Publications, London, 2008), pp. 67–86Google Scholar
  12. 12.
    R. Goré, Cut-free sequent and tableau systems for propositional diodorean modal logics. Studia Logica 53(3), 433–457 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    R. Goré, Machine checking proof theory: an application of logic to logic, in ICLA, Lecture Notes in Computer Science, ed. by R. Ramanujam, S. Sarukkai (Springer, New York, 2009), pp. 23–35Google Scholar
  14. 14.
    J. Goubault-Larrecq, On computational interpretations of the modal logic S4. I. Cut elimination. Technical report, Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe (1996)Google Scholar
  15. 15.
    A. Indrzejczak, Cut-free hypersequent calculus for S4.3. Bull. Sect. Logic 41(1–2), 89–104 (2012)MathSciNetzbMATHGoogle Scholar
  16. 16.
    G. Mints, Two examples of cut-elimination for non-classical logics. Talk at JägerFest (2013)Google Scholar
  17. 17.
    S. Negri, J. von Plato, Structural Proof Theory (Cambridge University Press, Cambridge, 2001)Google Scholar
  18. 18.
    S. Negri, Proof analysis in modal logic. J. Philos. Logic 34(5–6), 507–544 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    M. Ohnishi, K. Matsumoto, Gentzen method in modal calculi. Osaka Math. J. 9(2), 113–130 (1957)MathSciNetzbMATHGoogle Scholar
  20. 20.
    L. Paulson, Isabelle: A Generic Theorem Prover, vol. 828. LNCS (1994)Google Scholar
  21. 21.
    F. Pfenning, Structural cut elimination, in 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, 26–29 June 1995 (IEEE Computer Society, 1995), pp. 156–166Google Scholar
  22. 22.
    T. Shimura, Cut-free systems for the modal logic S4.3 and S4.3Grz. Rep. Math. Logic 25, 57–72 (1991)MathSciNetzbMATHGoogle Scholar
  23. 23.
    Special issue on formal proof. Notices of the American Mathematical Society, vol. 55, Dec 2008Google Scholar
  24. 24.
    H. Tews, Formalizing cut elimination of coalgebraic logics in coq, in Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2013. LNCS, vol. 8123 (2013), pp. 257–272Google Scholar
  25. 25.
    A. Troelstra, H. Schwichtenberg, Basic Proof Theory (Cambridge University Press, Cambridge, 2000)Google Scholar
  26. 26.
    M. Wenzel, T. Nipkow, L. Paulson, Isabelle/HOL. A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283 (2002)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Logic and Computation Group, School of Computer ScienceThe Australian National UniversityCanberraAustralia

Personalised recommendations