@@ -6,47 +6,48 @@ This website gives a brief overview of our [HOLMS library](https://github.com/HO
66
77- Marco Maggesi, Cosimo Perini Brogi (2021)<br />
88*** A Formal Proof of Modal Completeness for Provability Logic*** .<br />
9- In 12th International Conference on Interactive Theorem Proving (ITP 2021).<br />
9+ In 12th International Conference on Interactive Theorem Proving ([ ITP 2021] ( https://easyconferences.eu/itp2021/ ) ).<br />
1010 Leibniz International Proceedings in Informatics (LIPIcs),<br />
1111 Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)<br />
1212 DOI:[ 10.4230/LIPIcs.ITP.2021.26] ( https://doi.org/10.4230/LIPIcs.ITP.2021.26 ) (Open access)
1313
1414- Marco Maggesi, Cosimo Perini Brogi (2023)<br />
1515*** Mechanising Gödel–Löb Provability Logic in HOL Light*** .<br />
16- J Autom Reasoning 67, 29. DOI:[ 10.1007/s10817-023-09677-z] ( https://doi.org/10.1007/s10817-023-09677-z ) (Open access)
16+ J Autom Reasoning 67, 29.< br /> DOI:[ 10.1007/s10817-023-09677-z] ( https://doi.org/10.1007/s10817-023-09677-z ) (Open access)
1717
1818- Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini (2024)<br />
1919*** Growing HOLMS, a HOL Light Library for Modal Systems*** .<br />
20- [ OVERLAY 2024 ] ( https://overlay.uniud.it/workshop/2024/ ) - 6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis <br />
20+ In 6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis ( [ OVERLAY 2024 ] ( https://overlay.uniud.it/workshop/2024/ ) ) <br />
2121 28 and 29 November, Bolzano (Italy).<br />
2222 CEUR Workshop Proceedings, <br />
2323 Volume 3904, pp. 41-48, CEUR-WS.org (2024)<br />
24- [ Download] ( https://ceur-ws.org/Vol-3904/paper5.pdf ) (Open access)
24+ DBLP:[ conf/overlay/BilottaMBQ24] ( https://ceur-ws.org/Vol-3904/paper5.pdf ) (Open access)
25+
2526
2627- Antonella Bilotta (2025)<br />
2728*** Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library*** .<br />
2829 Master’s Thesis, Università degli Studi di Firenze, Firenze (Italy).<br />
29- [ Download (arXiv: 2506.10048) ] ( https://arxiv.org/abs/2506.10048 ) (Open access)
30+ DOI arxiv: [ 2506.10048] ( https://arxiv.org/abs/2506.10048 ) (Open access)
3031
3132- Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2025)<br />
3233*** Growing a Modular Framework for Modal Systems: HOLMS.*** .<br />
33- [ WiL 2025] ( https://sites.google.com/view/wil2025/home ) - 9th Women in Logic Workshop <br />
34+ In 9th Women in Logic Workshop ( [ WiL 2025] ( https://sites.google.com/view/wil2025/home ) ) <br />
3435 14 July, Birmingham (United Kingdom).<br />
3536 Book of Abstract of Women in Logic 2025, pp. 7-11. <br />
3637[ Download] ( https://liveuclac-my.sharepoint.com/:b:/g/personal/ucacepi_ucl_ac_uk/EdtzuTRYSm5DrdTU-XglSP8BZkR4N-x_KauVp2YiEsrqgg?e=IpzlMM ) (Open access)
3738
3839- Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2025)<br />
3940*** A Modular Proof of Semantic Completeness for Normal Systems beyond the Modal Cube, Formalised in HOLMS.*** .<br />
40- [ ICTCS 2025] ( https://ictcs2025.unich.it/ ) - 26th Italian Conference on Theoretical Computer Science <br />
41+ In 26th Italian Conference on Theoretical Computer Science ( [ ICTCS 2025] ( https://ictcs2025.unich.it/ ) ) <br />
4142 September 10-12, 2025, Pescara (Italy).<br />
4243 CEUR Workshop Proceedings, <br />
4344 Volume 4039, pp. 154-162, CEUR-WS.org (2025)<br />
44- [ Download ] ( https://ceur-ws.org/Vol-4039/paper10.pdf ) (Open access)
45+ DBLP: [ conf/ictcs/BilottaMB25 ] ( https://ceur-ws.org/Vol-4039/paper10.pdf ) (Open access)
4546
4647##Talks & Presentations
4748- ** [ OVERLAY 2024] ( https://overlay.uniud.it/workshop/2024/ ) ** – 6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis<br />
4849 28 and 29 November, Bolzano (Italy). <br />
49- [ Slides (PDF)] ( )
50+ [ Slides (PDF)] ( https://drive.google.com/file/d/1ys7VisacuYD2raSEuDXXUtfF7lEJN5BH/view?usp=sharing )
5051
5152- ** [ WiL 2025] ( https://sites.google.com/view/wil2025/home ) ** – 9th Women in Logic Workshop <br />
5253 14 July, Birmingham (United Kingdom). <br />
@@ -67,7 +68,7 @@ This website gives a brief overview of our [HOLMS library](https://github.com/HO
6768| Reference| Modal Logics|
6869| -------------------------------| ----------------------------|
6970| ** Journal of Automated Reasoning 63 (2023)** | GL|
70- | ** OVERLAY 2024 (2023 )** | GL, K|
71+ | ** OVERLAY 2024 (2024 )** | GL, K|
7172| ** Bilotta Master's Thesis (Spring 2025)** | GL, K, K4, T|
7273| ** WiL 2025, ICTCS 2025 (Summer 2025)** | GL, K, K4, T, S4, B, S5|
7374
@@ -79,5 +80,14 @@ This website gives a brief overview of our [HOLMS library](https://github.com/HO
7980- Leonardo Quartini, University of Florence, Italy
8081
8182
82- ##HOLMSUSAGE GUIDE
83+ ##HOLMSUsage Guide
8384The[ README.md] ( https://github.com/HOLMS-lib/HOLMS/blob/main/README.md ) provides a usage guide for our HOLMS library at its current status.
85+
86+
87+ ##HOL Light Mini-Manual
88+
89+ 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 ) .
90+ Useful for students, researchers, and contributors approaching** mechanisation in HOL Light** or in a** proof assistant** for the first time.
91+
92+ [ Read the Mini-Manual (PDF, arXiv)] ( https://arxiv.org/pdf/2506.10048.pdf#page=68 )
93+