- Marco Maggesi, Cosimo Perini Brogi (2021)<br/>

***A Formal Proof of Modal Completeness for Provability Logic***.<br/>

In 12th International Conference on Interactive Theorem Proving (ITP 2021).<br/>

In 12th International Conference on Interactive Theorem Proving ([ITP 2021](https://easyconferences.eu/itp2021/)).<br/>

Leibniz International Proceedings in Informatics (LIPIcs),<br/>

Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)<br/>

DOI:[10.4230/LIPIcs.ITP.2021.26](https://doi.org/10.4230/LIPIcs.ITP.2021.26) (Open access)

- Marco Maggesi, Cosimo Perini Brogi (2023)<br/>

***Mechanising Gödel–Löb Provability Logic in HOL Light***.<br/>

J Autom Reasoning 67, 29. DOI:[10.1007/s10817-023-09677-z](https://doi.org/10.1007/s10817-023-09677-z) (Open access)

J Autom Reasoning 67, 29.<br/> DOI:[10.1007/s10817-023-09677-z](https://doi.org/10.1007/s10817-023-09677-z) (Open access)

- Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini (2024)<br/>

***Growing HOLMS, a HOL Light Library for Modal Systems***.<br/>

[OVERLAY 2024](https://overlay.uniud.it/workshop/2024/) -6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis <br/>

In6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis ([OVERLAY 2024](https://overlay.uniud.it/workshop/2024/)) <br/>

28 and 29 November, Bolzano (Italy).<br/>

CEUR Workshop Proceedings, <br/>

Volume 3904, pp. 41-48, CEUR-WS.org (2024)<br/>

[Download](https://ceur-ws.org/Vol-3904/paper5.pdf) (Open access)

DBLP:[conf/overlay/BilottaMBQ24](https://ceur-ws.org/Vol-3904/paper5.pdf) (Open access)

- Antonella Bilotta (2025)<br/>

***Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library***.<br/>

Master’s Thesis, Università degli Studi di Firenze, Firenze (Italy).<br/>

[Download (arXiv:2506.10048)](https://arxiv.org/abs/2506.10048) (Open access)

DOI arxiv:[2506.10048](https://arxiv.org/abs/2506.10048) (Open access)

- Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2025)<br/>

***Growing a Modular Framework for Modal Systems: HOLMS.***.<br/>

[WiL 2025](https://sites.google.com/view/wil2025/home) - 9th Women in Logic Workshop <br/>

In 9th Women in Logic Workshop ([WiL 2025](https://sites.google.com/view/wil2025/home)) <br/>

14 July, Birmingham (United Kingdom).<br/>

Book of Abstract of Women in Logic 2025, pp. 7-11. <br/>

[Download](https://liveuclac-my.sharepoint.com/:b:/g/personal/ucacepi_ucl_ac_uk/EdtzuTRYSm5DrdTU-XglSP8BZkR4N-x_KauVp2YiEsrqgg?e=IpzlMM) (Open access)

- Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2025)<br/>

***A Modular Proof of Semantic Completeness for Normal Systems beyond the Modal Cube, Formalised in HOLMS.***.<br/>

[ICTCS 2025](https://ictcs2025.unich.it/) - 26th Italian Conference on Theoretical Computer Science <br/>

In 26th Italian Conference on Theoretical Computer Science ([ICTCS 2025](https://ictcs2025.unich.it/)) <br/>

September 10-12, 2025, Pescara (Italy).<br/>

CEUR Workshop Proceedings, <br/>

Volume 4039, pp. 154-162, CEUR-WS.org (2025)<br/>

[Download](https://ceur-ws.org/Vol-4039/paper10.pdf) (Open access)

DBLP:[conf/ictcs/BilottaMB25](https://ceur-ws.org/Vol-4039/paper10.pdf) (Open access)

-**[OVERLAY 2024](https://overlay.uniud.it/workshop/2024/)** – 6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis<br/>

28 and 29 November, Bolzano (Italy). <br/>

[Slides (PDF)](https://drive.google.com/file/d/1ys7VisacuYD2raSEuDXXUtfF7lEJN5BH/view?usp=sharing)

-**[WiL 2025](https://sites.google.com/view/wil2025/home)** – 9th Women in Logic Workshop <br/>

14 July, Birmingham (United Kingdom). <br/>

[Slides (PDF)](https://drive.google.com/file/d/1IU-zT0WePrNoYwhJFGfrahLi9APRbBOj/view)

-**[ICTCS 2025](https://ictcs2025.unich.it/)** – 26th Italian Conference on Theoretical Computer Science <br/>

September 10-12, Pescara (Italy).<br/>

[Slides (PDF)](https://drive.google.com/file/d/1niJI42GMCgGP7TfGVUtcw_NiGb8cqtM4/view)

-**[Proof and Computation 2025](https://www.mathematik.uni-muenchen.de/~schwicht/pc25.php)** - 9th Proof and Computation Autumn School <br/>

September 15-19, Herrsching am Ammersee (Deutschland). <br/>

[Slides (PDF)](https://drive.google.com/file/d/1zW_XKooRUQB4VSnLRZtj7O4OL32e6L3U/view)

**Modal Logics Mechanised in HOLMS** (chronological):

| Reference| Modal Logics|

|-------------------------------|----------------------------|

|**Journal of Automated Reasoning 63 (2023)**| GL|

|**OVERLAY 2024 (2024)**| GL, K|

|**Bilotta Master's Thesis (Spring 2025)**| GL, K, K4, T|

|**WiL 2025, ICTCS 2025 (Summer 2025)**| GL, K, K4, T, S4, B, S5|

- Leonardo Quartini, University of Florence, Italy

The[README.md](https://github.com/HOLMS-lib/HOLMS/blob/main/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](https://arxiv.org/abs/2506.10048).

Useful for students, researchers, and contributors approaching**mechanisation in HOL Light** or in a**proof assistant** for the first time.

[Read the Mini-Manual (PDF, arXiv)](https://arxiv.org/pdf/2506.10048.pdf#page=68)