This website gives a brief overview of the HOLMS library, a modular framework for implementing modal reasoning within the HOL Light theorem prover.
Marco Maggesi, Cosimo Perini Brogi (2021)
A Formal Proof of Modal Completeness for Provability Logic.
In 12th International Conference on Interactive Theorem Proving (ITP 2021)
June 29- July 1, 2021, Rome (Italy).
Leibniz International Proceedings in Informatics (LIPIcs)
Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik
DOI:10.4230/LIPIcs.ITP.2021.26 (Open access)
Marco Maggesi, Cosimo Perini Brogi (2023)
Mechanising Gödel–Löb Provability Logic in HOL Light.
J Autom Reasoning 67, 29.
DOI:10.1007/s10817-023-09677-z (Open access)
Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini (2024)
Growing HOLMS, a HOL Light Library for Modal Systems.
In 6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis (OVERLAY 2024)
28 and 29 November, Bolzano (Italy).
CEUR Workshop Proceedings,
Volume 3904, pp. 41-48, CEUR-WS.org
DBLP:conf/overlay/BilottaMBQ24 (Open access)
Antonella Bilotta (2025)
Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library.
Master’s Thesis, Università degli Studi di Firenze, Firenze (Italy).
DOI arxiv: 2506.10048 (Open access)
Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2025)
Growing a Modular Framework for Modal Systems: HOLMS.
In 9th Women in Logic Workshop (WiL 2025)
14 July, Birmingham (United Kingdom).
Book of Abstract of Women in Logic 2025, pp. 7-11.
Extended Abstract, Download (Open access)
Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2025)
A Modular Proof of Semantic Completeness for Normal Systems beyond the Modal Cube, Formalised in HOLMS.
In 26th Italian Conference on Theoretical Computer Science (ICTCS 2025)
September 10-12, 2025, Pescara (Italy).
CEUR Workshop Proceedings,
Volume 4039, pp. 154-162, CEUR-WS.org
DBLP:conf/ictcs/BilottaMB25 (Open access)
Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2026)
A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light.
In Proceedings of the 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)
February 24-27, 2026, Paris (France).
Leibniz International Proceedings in Informatics (LIPIcs)
Volume 363, pp. 18:1–18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik
DOI:10.4230/LIPIcs.CSL.2026.18 (Open access)
Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2026, to appear)
Growing HOLMS: Grzegorczyk Logic and Experiments with Translations in HOL Light.
In 10th Women in Logic Workshop (WiL 2026)
July 24-25, 2026, Lisbon (Portugal). (Extended Abstract)
Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2026, to appear)
Growing HOLMS: A Verified Automated Prover for Grzegorczyk Logic in HOL Light.
In Proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2026)
July 26-29, 2026, Lisbon (Portugal).
OVERLAY 2024 – 6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis
28 and 29 November, Bolzano (Italy).
Slides (PDF)
WiL 2025 – 9th Women in Logic Workshop
14 July, Birmingham (United Kingdom).
Slides (PDF) & Abstract (PDF)
ICTCS 2025 – 26th Italian Conference on Theoretical Computer Science
September 10-12, Pescara (Italy).
Slides (PDF)
Proof and Computation 2025 - 9th Proof and Computation Autumn School
September 15-19, Herrsching am Ammersee (Deutschland).
Slides (PDF)
CSL 2026 - 34th EACSL Annual Conference on Computer Science Logic
February 24-27, Paris (France).
Slides (PDF)
Modal Logics Mechanised in HOLMS (chronological):
| Reference | Modal Logics | Other Improvements | Observations |
|---|---|---|---|
| Journal of Automated Reasoning 63 2023 | GL | ||
| OVERLAY 2024 | GL, K | ||
| Bilotta Master’s Thesis | GL, K, K4, T | Modular Design ✓ | Semidecision for K4 |
| WiL 2025, ICTCS 2025, CSL 2026 | GL, K, K4, T, S4, B, S5 | Certified Countermodels ✓ | Semidecision for K4, S4, S5 |
| IJCAR 2026, WiL 2026 (to appear) | GL, K, K4, T, S4, B, S5, Grz | Modal Translation ✓ | Non-Modular Completeness Proof for Grz |
| Last Developments | GL, K, K4, T, S4, B, S5, Grz, D | Modular Completeness for Grz ✓ |
The README.md provides a usage guide for our HOLMS library at its current status.
A 30-page introductory guide for non-specialists, taken from Chapter 2 of Antonella Bilotta’s Master’s Thesis.
Useful for students, researchers, and contributors approaching mechanisation in HOL Light or in a proof assistant for the first time.