This website gives a brief overview of our HOLMS library for 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).
Leibniz International Proceedings in Informatics (LIPIcs),
Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
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 (2024)
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.
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 (2025)
DBLP:conf/ictcs/BilottaMB25 (Open access)
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)
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)
Modal Logics Mechanised in HOLMS (chronological):
| Reference | Modal Logics | Other Improvements |
|---|---|---|
| Journal of Automated Reasoning 63 (2023) | GL | |
| OVERLAY 2024 (2024) | GL, K | |
| Bilotta Master’s Thesis (Spring 2025) | GL, K, K4, T | Modular Design ✓ |
| WiL 2025, ICTCS 2025 (Summer 2025) | GL, K, K4, T, S4, B, S5 | |
| CSL 2026 (To appear in 2026) | GL, K, K4, T, S4, B, S5 | Certified Countermodels ✓ |
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.