Document Open Access Logo

A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light

Authors Antonella Bilotta , Marco Maggesi , Cosimo Perini Brogi

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.18.pdf
  • Filesize: 1.24 MB
  • 29 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Higher order logic
  • Theory of computation → Automated reasoning
  • Theory of computation → Type theory
  • Theory of computation → Proof theory
  • Theory of computation → Logic and verification
Keywords
  • Modal logic
  • HOL Light
  • Labelled sequent calculi
  • Logical verification
  • Interactive theorem proving
  • Automated proof-search

Metrics

Abstract

We extend the existing HOL Light Library for Modal Systems (HOLMS) to support a modular implementation of modal reasoning within the HOL Light proof assistant. We deeply embed axiomatic calculi and relational semantics for seven normal modal logics (K, T, B, K4, S4, S5, GL) and formalise modal adequacy theorems for these systems. We then leverage those formalisations to implement a mechanism for automated reasoning via proof-search in the associated labelled sequent calculi, which we shallowly embed in HOL Light’s goal-stack mechanism. This way, we equip the general-purpose proof assistant with (semi)decision procedures for these logics that, in case of failure to construct a proof for the input formula, return a certified countermodel within the appropriate class for the logic under consideration. On the methodological side, we propose a precise measure of the modularity of our approach by systematically adopting Christopher Strachey’s distinction between ad hoc and parametric polymorphism throughout the library.

Cite As Get BibTex

Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.18

Author Details

Antonella Bilotta
  • Scuola Normale Superiore di Pisa, Italy
Marco Maggesi
  • University of Florence, Italy
Cosimo Perini Brogi
  • IMT School for Advanced Studies Lucca, Italy

Funding

This work was partially funded by the project SERICS - Security and Rights in the CyberSpace PE0000014, financed within PNRR, M4C2 I.1.3, funded by the European Union - NextGenerationEU (MUR Code: 2022CY2J5S, CUP: D67G22000340001); the Istituto Nazionale di Alta Matematica - INdAM group GNSAGA; the EC-COST Action (CA20111) "EuroProofNet"; the research project "Differential, Algebraic, Complex and Arithmetic Geometry (2025)"; The International Research Network "Logic and Interaction".
  • Maggesi, Marco: Istituto Nazionale di Alta Matematica - INdAM group GNSAGA.
  • Perini Brogi, Cosimo: The project SERICS - Security and Rights in the CyberSpace PE0000014, financed within PNRR, M4C2 I.1.3, funded by the European Union - NextGenerationEU (MUR Code: 2022CY2J5S); The International Research Network "Logic and Interaction".

Acknowledgements

We thank three anonymous reviewers for their valuable and constructive feedback on our original submission.

Supplementary Materials

References

  1. Oskar Abrahamsson, Magnus O. Myreen, Ramana Kumar, and Thomas Sewell. Candle: A Verified Implementation of HOL Light. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1-3:17, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.3.
  2. Matteo Acclavio, Fabrizio Montesi, and Marco Peressotti. On propositional dynamic logic and concurrency. arXiv preprint arXiv:2403.18508, 2024. URL: https://doi.org/10.48550/arXiv.2403.18508.
  3. Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, and Jiri Srba. Reactive systems: modelling, specification and verification. Cambridge University Press, 2007. Google Scholar
  4. Bahareh Afshari, Sebastian Enqvist, Graham E Leigh, Johannes Marti, and Yde Venema. Proof systems for two-way modal mu-calculus. The Journal of Symbolic Logic, pages 1-50, 2023. Google Scholar
  5. Bahareh Afshari, Graham E Leigh, and Guillermo Menéndez Turata. A cyclic proof system for full computation tree logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.5.
  6. Andrew W Appel, Paul-André Mellies, Christopher D Richards, and Jérôme Vouillon. A very modal model of a modern, major, general type system. In Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 109-122, 2007. URL: https://doi.org/10.1145/1190216.1190235.
  7. David Basin, Cas Cremers, and Catherine Meadows. Model Checking Security Protocols, pages 727-762. Springer International Publishing, Cham, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_22.
  8. David A. Basin, Seán Matthews, and Luca Viganò. Labelled Propositional Modal Logics: Theory and Practice. J. Log. Comput., 7(6):685-717, 1997. URL: https://doi.org/10.1093/LOGCOM/7.6.685.
  9. Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. Journal of logical and algebraic methods in programming, 84(1):108-123, 2015. URL: https://doi.org/10.1016/J.JLAMP.2014.02.001.
  10. Bernhard Beckert and Joachim Posegga. leanTAP: Lean Tableau-based Deduction. J. Autom. Reason., 15(3):339-358, 1995. URL: https://doi.org/10.1007/BF00881804.
  11. Christoph Benzmueller and Lawrence C. Paulson. Multimodal and intuitionistic logics in simple type theory. Logic Journal of the IGPL, 18(6):881-892, January 2010. URL: https://doi.org/10.1093/jigpal/jzp080.
  12. Christoph Benzmüller. Universal (meta-)logical reasoning: Recent successes. Sci. Comput. Program., 172:48-62, 2019. URL: https://doi.org/10.1016/J.SCICO.2018.10.008.
  13. Christoph Benzmüller. Faithful logic embeddings in HOL - A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level. CoRR, abs/2502.19311, 2025. URL: https://doi.org/10.48550/arXiv.2502.19311.
  14. Christoph Benzmüller, Maximilian Claus, and Nik Sultana. Systematic Verification of the Modal Logic Cube in Isabelle/HOL. In Cezary Kaliszyk and Andrei Paskevich, editors, Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015, volume 186 of EPTCS, pages 27-41, 2015. URL: https://doi.org/10.4204/EPTCS.186.5.
  15. Christoph Benzmüller and Bruno Woltzenlogel Paleo. Higher-Order Modal Logics: Automation and Applications. In Wolfgang Faber and Adrian Paschke, editors, Reasoning Web. Web Logic Rules - 11th International Summer School 2015, Berlin, Germany, July 31 - August 4, 2015, Tutorial Lectures, volume 9203 of Lecture Notes in Computer Science, pages 32-74. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21768-0_2.
  16. Christoph Benzmüller, Xavier Parent, and Leendert W. N. van der Torre. Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. Artif. Intell., 287:103348, 2020. URL: https://doi.org/10.1016/J.ARTINT.2020.103348.
  17. Christoph Benzmüller and Lawrence C. Paulson. Quantified multimodal logics in simple type theory. Logica Universalis, 7(1):7-20, 2013. URL: https://doi.org/10.1007/S11787-012-0052-Y.
  18. Christoph Benzmüller and Dana Scott. Notes on Gödel’s and Scott’s variants of the ontological argument. Monatshefte für Mathematik, pages 1-43, 2025. Google Scholar
  19. Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. HOLMS: A HOL Light Library for Modal Systems. Software, (visited on 2026-02-02). URL: https://github.com/HOLMS-lib/HOLMS
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.25484
  20. Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. A Modular Proof of Semantic Completeness for Normal Systems beyond the Modal Cube, Formalised in HOLMS. In Luca Moscardelli and Francesca Scozzari, editors, Proceedings of the 26th Italian Conference on Theoretical Computer Science, Pescara, Italy, September 10-12, 2025, volume 4039 of CEUR Workshop Proceedings, pages 154-162. CEUR-WS.org, 2025. URL: https://ceur-ws.org/Vol-4039/paper10.pdf.
  21. Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. Webpage of HOLMS: A HOL Light Library for Modal Systems, 2025. Software (visited on 2026-02-02). URL: https://holms-lib.github.io/
    full metadata available at: https://doi.org/10.4230/artifacts.25485
  22. Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, and Leonardo Quartini. Growing HOLMS, a HOL Light Library for Modal Systems. In Daniele Porello, Cosimo Vinci, and Matteo Zavatteri, editors, Short Paper Proceedings of the 6th International Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, OVERLAY 2024, Bolzano, Italy, November 28-29, 2024, volume 3904 of CEUR Workshop Proceedings, pages 41-48. CEUR-WS.org, 2024. URL: https://ceur-ws.org/Vol-3904/paper5.pdf.
  23. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. URL: https://doi.org/10.1017/CBO9781107050884.
  24. Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors. Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning. North-Holland, 2007. URL: https://www.sciencedirect.com/bookseries/studies-in-logic-and-practical-reasoning/vol/3/suppl/C.
  25. George Boolos. The logic of provability. Cambridge University Press, 1995. Google Scholar
  26. Riccardo Borsetto and Margherita Zorzi. An Agda Implementation of the Modal Logic S4.2: First Investigations. In Luca Moscardelli and Francesca Scozzari, editors, Proceedings of the 26th Italian Conference on Theoretical Computer Science, Pescara, Italy, September 10-12, 2025, volume 4039 of CEUR Workshop Proceedings, pages 163-168. CEUR-WS.org, 2025. URL: https://ceur-ws.org/Vol-4039/paper17.pdf.
  27. Riccardo Borsetto and Margherita Zorzi. NAMOR: a New Agda Library for Modal Extended Sequents. In Short Paper Proceedings of the 7th International Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, OVERLAY 2025, Bologna, Italy, October 26, 2025, 2025. URL: https://overlay.uniud.it/workshop/2025/papers/borsetto-zorzi.pdf.
  28. Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551-577, 2009. URL: https://doi.org/10.1007/S00153-009-0137-3.
  29. Julie Cailler. Designing an Automated Concurrent Tableau-Based Theorem Prover for First-Order Logic. (Conception d'un prouveur automatique de théorèmes concurrent basé sur la méthode des tableaux pour la logique du premier ordre). PhD thesis, University of Montpellier, France, 2023. URL: https://tel.archives-ouvertes.fr/tel-04526940.
  30. Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard, and Hinde-Lilia Bouziane. Goéland: A Concurrent Tableau-Based Theorem Prover (System Description). In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 359-368. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_22.
  31. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Dexter Kozen, editor, Logics of Programs, pages 52-71, Berlin, Heidelberg, 1982. Springer Berlin Heidelberg. Google Scholar
  32. E.M. Clarke, O. Grumberg, D. Peled, and D.A. Peled. Model Checking. The Cyber-Physical Systems Series. MIT Press, 1999. Google Scholar
  33. Gabriele Costa and Cosimo Perini Brogi. Toward dynamic epistemic verification of zero-knowledge protocols. In Gianni D'Angelo, Flaminia L. Luccio, and Francesco Palmieri, editors, Proceedings of the 8th Italian Conference on Cyber Security (ITASEC 2024), Salerno, Italy, April 8-12, 2024, volume 3731 of CEUR Workshop Proceedings. CEUR-WS.org, 2024. URL: https://ceur-ws.org/Vol-3731/paper25.pdf.
  34. Tiziano Dalmonte, Sara Negri, Nicola Olivetti, and Gian Luca Pozzato. Theorem Proving for Non-normal Modal Logics. In OVERLAY 2020, Udine, Italy, September 2021. URL: https://hal.archives-ouvertes.fr/hal-03159954.
  35. Tiziano Dalmonte, Sara Negri, Nicola Olivetti, Gian Luca Pozzato, and Cyril Terrioux. PRONOM: A theorem prover for nonnormal modal logics. Available at http://193.51.60.97:8000/pronom/, 2025.
  36. Tiziano Dalmonte, Nicola Olivetti, and Sara Negri. Non-normal modal logics: Bi-neighbourhood semantics and its labelled calculi. In Advances in Modal Logic 2018, 2018. Google Scholar
  37. Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato, and Cyril Terrioux. HYPNO theorem proving with hypersequent calculi for non-normal modal logics. Available at http://193.51.60.97:8000/HYPNO/, 2025.
  38. Anupam Das and Sonia Marin. On intuitionistic diamonds (and lack thereof). In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 283-301. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43513-3_16.
  39. Anupam Das, Iris van der Giessen, and Sonia Marin. Intuitionistic Gödel-Löb logic, à la Simpson: Labelled systems and birelational semantics. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024, February 19-23, 2024, Naples, Italy, volume 288 of LIPIcs, pages 22:1-22:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CSL.2024.22.
  40. Jim de Groot, Ian Shillito, and Ranald Clouston. Semantical analysis of intuitionistic modal logics between CK and IK. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 169-182. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00020.
  41. Simon Docherty and Reuben NS Rowe. A non-wellfounded, labelled proof system for propositional dynamic logic. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 335-352. Springer, 2019. Google Scholar
  42. Christian Doczkal and Joachim Bard. Completeness and decidability of converse PDL in the constructive type theory of Coq. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 42-52, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3167088.
  43. Christian Doczkal and Gert Smolka. Constructive formalization of hybrid logic with eventualities. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, pages 5-20, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-25379-9_3.
  44. Christian Doczkal and Gert Smolka. Completeness and decidability results for CTL in constructive type theory. Journal of Automated Reasoning, 56(3):343-365, 2016. URL: https://doi.org/10.1007/S10817-016-9361-9.
  45. Hugo Férée, Iris van der Giessen, Sam van Gool, and Ian Shillito. Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II, volume 14740 of Lecture Notes in Computer Science, pages 43-60. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63501-4_3.
  46. Melvin Fitting. Proof methods for modal and intuitionistic logics, volume 169. Springer Science & Business Media, 2013. Google Scholar
  47. Asta Halkjær From. Formalized Soundness and Completeness of Epistemic Logic. In Alexandra Silva, Renata Wassermann, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 27th International Workshop, WoLLIC 2021, Virtual Event, October 5-8, 2021, Proceedings, volume 13038 of Lecture Notes in Computer Science, pages 1-15. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-88853-4_1.
  48. Asta Halkjær From. An Isabelle/HOL Framework for Synthetic Completeness Proofs. In Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP '25, pages 171-186, New York, NY, USA, 2025. Association for Computing Machinery. URL: https://doi.org/10.1145/3703595.3705882.
  49. Deepak Garg, Valerio Genovese, and Sara Negri. Countermodels from sequent calculi in multi-modal logics. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 315-324. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.42.
  50. James Garson. Modal Logic. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Spring 2024 edition, 2024. Google Scholar
  51. Marianna Girlando, Bjoern Lellmann, Nicola Olivetti, Stefano Pesce, and Gian Luca Pozzato. Theorem proving for Lewis Logics of Counterfactual Reasoning. In CILC 2020 - 35th Edition of the Italian Conference on Computational Logic, Rende / Virtual, Italy, October 2020. URL: https://hal.science/hal-03080670.
  52. Marianna Girlando, Bjoern Lellmann, Nicola Olivetti, Gian Luca Pozzato, and Quentin Vitalis. VINTE: an implementation of internal calculi for Lewis’ logics of counterfactual reasoning. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 149-159. Springer, 2017. Google Scholar
  53. Marianna Girlando, Björn Lellmann, Nicola Olivetti, Stefano Pesce, and Gian Luca Pozzato. Calculi, countermodel generation and theorem prover for strong logics of counterfactual reasoning. Journal of Logic and Computation, January 2022. exab084. URL: https://doi.org/10.1093/logcom/exab084.
  54. Marianna Girlando and Marianela Morales. MOILab: towards a labelled theorem prover for intuitionistic modal logics. working paper or preprint, December 2020. URL: https://hal.science/hal-03048966.
  55. Marianna Girlando and Marianela Morales. MOILab: a prototype theorem prover for intuitionistic modal logic IK based on labelled sequents. Available at https://www.mariannagirlando.com/MOILab.html, 2025.
  56. Marianna Girlando, Sara Negri, Nicola Olivetti, and Vincent Risch. Conditional beliefs: from neighbourhood semantics to sequent calculus. The review of symbolic logic, 11(4):736-779, 2018. URL: https://doi.org/10.1017/S1755020318000023.
  57. Marianna Girlando and Lutz Straßburger. Moin: A nested sequent theorem prover for intuitionistic modal logics (system description). In International Joint Conference on Automated Reasoning, pages 398-407. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_25.
  58. Rajeev Goré and Jack Kelly. Automated proof search in Gödel-Löb provability logic. In abstract, British Logic Colloquium, 2007. Google Scholar
  59. Rajeev Goré and Cormac Kikkert. CEGAR-Tableaux: improved modal satisfiability via modal clause-learning and SAT. In Automated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings 30, pages 74-91. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-86059-2_5.
  60. Rajeev Goré, Revantha Ramanayake, and Ian Shillito. Cut-elimination for provability logic by terminating proof-search: Formalised and deconstructed using coq. In Anupam Das and Sara Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 299-313, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-86059-2_18.
  61. Christian Hagemeier. Formalizing intuitionistic epistemic logic in Coq. BSc thesis, 2021. Google Scholar
  62. Christian Hagemeier and Dominik Kirst. Constructive and mechanised meta-theory of IEL and similar modal logics. J. Log. Comput., 32(8):1585-1610, 2022. URL: https://doi.org/10.1093/LOGCOM/EXAC068.
  63. Christian Hagemeier and Dominik Kirst. Constructive and mechanised meta-theory of intuitionistic epistemic logic. In Sergei N. Artëmov and Anil Nerode, editors, Logical Foundations of Computer Science - International Symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022, Proceedings, volume 13137 of Lecture Notes in Computer Science, pages 90-111. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-93100-1_7.
  64. Joseph Y. Halpern, Yoram Moses, and Mark R. Tuttle. A knowledge-based analysis of zero knowledge (preliminary report). In Janos Simon, editor, Proceedings of the 20th Annual ACM Symposium on Theory of Computing, May 2-4, 1988, Chicago, Illinois, USA, pages 132-147. ACM, 1988. URL: https://doi.org/10.1145/62212.62224.
  65. Moritz Hardt and Gert Smolka. Higher-order syntax and saturation algorithms for hybrid logic. In Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva, and Jørgen Villadsen, editors, Proceedings of the International Workshop on Hybrid Logic, HyLo@FLoC 2006, Seattle, WA, USA, August 11, 2006, volume 174(6) of Electronic Notes in Theoretical Computer Science, pages 15-27. Elsevier, 2006. URL: https://doi.org/10.1016/J.ENTCS.2006.11.023.
  66. John Harrison. HOL Light tutorial. http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf, 2017.
  67. John Harrison. The HOL Light system reference. https://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf, 2023.
  68. John Harrison. The HOL Light Theorem Prover. Official webpage: https://hol-light.github.io/, 2025.
  69. Ullrich Hustadt, Fabio Papacchini, Cláudia Nalon, and Clare Dixon. Model construction for modal clauses. In International Joint Conference on Automated Reasoning, pages 3-23. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63501-4_1.
  70. Andrzej Indrzejczak. Sequents and trees. Studies in Universal Logic, Birkhäuser, Cham, 2021. Google Scholar
  71. Dominik Kirst and Ian Shillito. Completeness of first-order bi-intuitionistic logic. In Jörg Endrullis and Sylvain Schmitz, editors, 33rd EACSL Annual Conference on Computer Science Logic, CSL 2025, February 10-14, 2025, Amsterdam, Netherlands, volume 326 of LIPIcs, pages 40:1-40:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CSL.2025.40.
  72. Roman Kuznets. Communication modalities. In Ludovic Levy Patey, Elaine Pimentel, Lorenzo Galeotti, and Florin Manea, editors, Twenty Years of Theoretical and Practical Synergies, pages 60-71, Cham, 2024. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-64309-5_6.
  73. Lara Lawniczak and Christoph Benzmüller. Logical Modalities within the European AI Act: An Analysis, 2025. Google Scholar
  74. Daan Leijen and Erik Meijer. Domain-Specific embedded compilers. In 2nd Conference on Domain-Specific Languages (DSL 99), Austin, TX, October 1999. USENIX Association. URL: https://www.usenix.org/conference/dsl-99/domain-specific-embedded-compilers.
  75. Ioana Leustean and Bogdan Macovei. DELP: Dynamic epistemic logic for security protocols. 2021 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pages 275-282, 2021. URL: https://api.semanticscholar.org/CorpusID:237491844.
  76. Marco Maggesi and Cosimo Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.26.
  77. Marco Maggesi and Cosimo Perini Brogi. Mechanising Gödel-Löb Provability Logic in HOL Light. J. Autom. Reason., 67(3):29, 2023. URL: https://doi.org/10.1007/S10817-023-09677-Z.
  78. Sonia Marin, Marianela Morales, and Lutz Straßburger. A fully labelled proof system for intuitionistic modal logics. J. Log. Comput., 31(3):998-1022, 2021. URL: https://doi.org/10.1093/LOGCOM/EXAB020.
  79. Simone Martini, Andrea Masini, and Margherita Zorzi. Cut elimination for extended sequent calculi. Bulletin of the Section of Logic, 52(4):459-495, 2023. URL: https://doi.org/10.18778/0138-0680.2023.22.
  80. Luka Mikec. Satisfiability verifiers for certain modal logics concerned with provability. Available at https://luka.doublebuffer.net/o/il/; Accessed: December 2025, 2025. URL: https://github.com/luka-mikec/provability_sat.
  81. Hiroshi Nakano. A modality for recursion. In Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332), pages 255-266. IEEE, 2000. URL: https://doi.org/10.1109/LICS.2000.855774.
  82. Cláudia Nalon. Efficient Theorem-Proving for Modal Logics. In Agata Ciabattoni, David Gabelaia, and Igor Sedlár, editors, Advances in Modal Logic, AiML 2024, Prague, Czech Republic, August 19-23, 2024, pages 13-16. College Publications, 2024. Google Scholar
  83. Cláudia Nalon, Clare Dixon, and Ullrich Hustadt. Modal resolution: proofs, layers, and refinements. ACM Transactions on Computational Logic (TOCL), 20(4):1-38, 2019. URL: https://doi.org/10.1145/3331448.
  84. Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, and Clare Dixon. Local reductions for the modal cube. In International Joint Conference on Automated Reasoning, pages 486-505. Springer International Publishing Cham, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_29.
  85. Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, and Clare Dixon. Buy one get 14 free: Evaluating local reductions for modal logic. In Brigitte Pientka and Cesare Tinelli, editors, Automated Deduction - CADE 29, pages 382-400, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-38499-8_22.
  86. Sara Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34(5):507-544, 2005. URL: https://doi.org/10.1007/S10992-005-2267-3.
  87. Sara Negri. Kripke Completeness Revisited. In Giuseppe Primiero, editor, Acts of Knowledge: History, Philosophy and Logic, pages 233-266. College Publications, 2009. Google Scholar
  88. Sara Negri. Proofs and countermodels in non-classical logics. Logica Universalis, 8(1):25-60, 2014. URL: https://doi.org/10.1007/S11787-014-0097-1.
  89. Sara Negri and Jan von Plato. Structural proof theory. Cambridge university press, 2008. Google Scholar
  90. Sara Negri and Jan von Plato. Proof analysis: a contribution to Hilbert’s last problem. Cambridge University Press, 2011. Google Scholar
  91. Nicola Olivetti and Gian Luca Pozzato. NESCOND: an implementation of nested sequent calculi for conditional logics. In International Joint Conference on Automated Reasoning, pages 511-518. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08587-6_39.
  92. Petros Papapanagiotou and Jacques Fleuriot. Object-Level Reasoning with Logics Encoded in HOL Light. In Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pages 18-34. Open Publishing Association, 2021. Google Scholar
  93. Dirk Pattinson, Nicola Olivetti, and Cláudia Nalon. Resolution calculi for non-normal modal logics. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 322-341. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43513-3_18.
  94. Cosimo Perini Brogi, Rocco De Nicola, and Omar Inverso. Simpson’s proof systems for process verification: A fine-tuning (short paper). In Ugo de'Liguoro, Matteo Palazzo, and Luca Roversi, editors, Proceedings of the 25th Italian Conference on Theoretical Computer Science, Torino, Italy, September 11-13, 2024, volume 3811 of CEUR Workshop Proceedings, pages 292-299. CEUR-WS.org, 2024. URL: https://ceur-ws.org/Vol-3811/paper050.pdf.
  95. Cosimo Perini Brogi, Sara Negri, and Nicola Olivetti. Modular Sequent Calculi for Interpretability Logics. Rev. Symb. Log., 18(3):704-743, 2025. URL: https://doi.org/10.1017/S1755020325100701.
  96. Gordon Plotkin and Matija Pretnar. A logic for algebraic effects. In 2008 23rd Annual IEEE symposium on logic in computer science, pages 118-129. IEEE, 2008. URL: https://doi.org/10.1109/LICS.2008.45.
  97. Francesca Poggiolesi. The method of tree-hypersequents for modal propositional logic. In Towards mathematical philosophy, pages 31-51. Springer, 2009. URL: https://doi.org/10.1007/978-1-4020-9084-4_3.
  98. Francesca Poggiolesi. Gentzen calculi for modal propositional logic, volume 32. Springer Science & Business Media, 2010. Google Scholar
  99. John Power. Generic models for computational effects. Theoretical Computer Science, 364(2):254-269, 2006. URL: https://doi.org/10.1016/J.TCS.2006.08.006.
  100. F. Rajaona, I. Boureanu, R. Ramanujam, and S. Wesemeyer. Epistemic model checking for privacy. In 2024 IEEE 37th Computer Security Foundations Symposium (CSF), pages 1-16, Los Alamitos, CA, USA, July 2024. IEEE Computer Society. URL: https://doi.org/10.1109/CSF61375.2024.00020.
  101. Jan Rooduijn, Dexter Kozen, and Alexandra Silva. A cyclic proof system for Guarded Kleene Algebra with Tests. In International Joint Conference on Automated Reasoning, pages 257-275. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63501-4_14.
  102. Renate Schmidt. Advances in Modal Logic Tools. Last modified: 03 Mar 23; Accessed: December 2025, 2025. URL: https://www.cs.man.ac.uk/~schmidt/tools/.
  103. Ian Shillito and Dominik Kirst. A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 218-229. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636957.
  104. Ian Shillito, Iris van der Giessen, Rajeev Goré, and Rosalie Iemhoff. A New Calculus for Intuitionistic Strong Löb Logic: Strong Termination and Cut-Elimination, Formalised. In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings, volume 14278 of Lecture Notes in Computer Science, pages 73-93. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43513-3_5.
  105. Alex K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics, 1994. Google Scholar
  106. Alex K. Simpson. Compositionality via cut-elimination: Hennessy-milner logic for an arbitrary GSOS. In Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA, June 26-29, 1995, pages 420-430. IEEE Computer Society, 1995. URL: https://doi.org/10.1109/LICS.1995.523276.
  107. Alex K. Simpson. Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS. J. Log. Algebraic Methods Program., 60-61:287-322, 2004. URL: https://doi.org/10.1016/J.JLAP.2004.03.004.
  108. Craig Smorynski. The incompleteness theorems. In Jon Barwise, editor, Handbook of mathematical logic, pages 821-865. North-Holland, 1977. Google Scholar
  109. Alexander Steen and Christoph Benzmüller. Challenges for Non-Classical Reasoning in Contemporary AI Applications. Künstliche Intelligenz, 38(1-2):7-16, 2024. URL: https://doi.org/10.1007/S13218-024-00855-8.
  110. Alexander Steen, Geoff Sutcliffe, and Christoph Benzmüller. Solving quantified modal logic problems by translation to classical logics. Journal of Logic and Computation, page exaf006, 2025. Google Scholar
  111. Colin Stirling. Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, 2001. URL: https://doi.org/10.1007/978-1-4757-3550-5.
  112. Colin Stirling. Bisimulation and logic, pages 173-196. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2011. Google Scholar
  113. Christopher Strachey. Fundamental concepts in programming languages. Higher-order and symbolic computation, 13:11-49, 2000. URL: https://doi.org/10.1023/A:1010000313106.
  114. Alfred Tarski. Undecidable Theories. North-Holland Pub. Co., Amsterdam, 1968. Google Scholar
  115. Anne Sjerp Troelstra and Helmut Schwichtenberg. Basic proof theory, Second Edition, volume 43 of Cambridge tracts in theoretical computer science. Cambridge University Press, 2000. Google Scholar
  116. Johan Van Benthem. Correspondence Theory, pages 325-408. Springer Netherlands, Dordrecht, 2001. URL: https://doi.org/10.1007/978-94-017-0454-0_4.
  117. Rineke (L.C.) Verbrugge. Provability Logic. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2024 edition, 2024. Google Scholar
  118. Luca Viganò. Labelled non-classical logics. Springer Science & Business Media, 2013. Google Scholar
  119. Minchao Wu and Rajeev Goré. Verified Decision Procedures for Modal Logics. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:19, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.31.
  120. Yiming Xu and Michael Norrish. Mechanised modal model theory. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 518-533, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-51074-9_30.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact