Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings

Commit5b32e11

Browse files
Merge pull request#2 from HOLMS-lib/Updated-Website
Update website with new pubblications and affiliation.md
2 parents0fecc48 +c7e798d commit5b32e11

File tree

1 file changed

+68
-6
lines changed

1 file changed

+68
-6
lines changed

‎index.md‎

Lines changed: 68 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,26 +6,88 @@ 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)
13+
1314
- Marco Maggesi, Cosimo Perini Brogi (2023)<br/>
1415
***Mechanising Gödel–Löb Provability Logic in HOL Light***.<br/>
15-
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)
17+
1618
- Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini (2024)<br/>
1719
***Growing HOLMS, a HOL Light Library for Modal Systems***.<br/>
18-
[OVERLAY 2024](https://overlay.uniud.it/workshop/2024/) -6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis <br/>
20+
In6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis ([OVERLAY 2024](https://overlay.uniud.it/workshop/2024/)) <br/>
1921
28 and 29 November, Bolzano (Italy).<br/>
20-
[Download](https://overlay.uniud.it/workshop/2024/papers/paper5.pdf).
22+
CEUR Workshop Proceedings, <br/>
23+
Volume 3904, pp. 41-48, CEUR-WS.org (2024)<br/>
24+
DBLP:[conf/overlay/BilottaMBQ24](https://ceur-ws.org/Vol-3904/paper5.pdf) (Open access)
25+
26+
27+
- Antonella Bilotta (2025)<br/>
28+
***Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library***.<br/>
29+
Master’s Thesis, Università degli Studi di Firenze, Firenze (Italy).<br/>
30+
DOI arxiv:[2506.10048](https://arxiv.org/abs/2506.10048) (Open access)
31+
32+
- Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2025)<br/>
33+
***Growing a Modular Framework for Modal Systems: HOLMS.***.<br/>
34+
In 9th Women in Logic Workshop ([WiL 2025](https://sites.google.com/view/wil2025/home)) <br/>
35+
14 July, Birmingham (United Kingdom).<br/>
36+
Book of Abstract of Women in Logic 2025, pp. 7-11. <br/>
37+
[Download](https://liveuclac-my.sharepoint.com/:b:/g/personal/ucacepi_ucl_ac_uk/EdtzuTRYSm5DrdTU-XglSP8BZkR4N-x_KauVp2YiEsrqgg?e=IpzlMM) (Open access)
38+
39+
- Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi (2025)<br/>
40+
***A Modular Proof of Semantic Completeness for Normal Systems beyond the Modal Cube, Formalised in HOLMS.***.<br/>
41+
In 26th Italian Conference on Theoretical Computer Science ([ICTCS 2025](https://ictcs2025.unich.it/)) <br/>
42+
September 10-12, 2025, Pescara (Italy).<br/>
43+
CEUR Workshop Proceedings, <br/>
44+
Volume 4039, pp. 154-162, CEUR-WS.org (2025)<br/>
45+
DBLP:[conf/ictcs/BilottaMB25](https://ceur-ws.org/Vol-4039/paper10.pdf) (Open access)
46+
47+
##Talks & Presentations
48+
-**[OVERLAY 2024](https://overlay.uniud.it/workshop/2024/)** – 6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis<br/>
49+
28 and 29 November, Bolzano (Italy). <br/>
50+
[Slides (PDF)](https://drive.google.com/file/d/1ys7VisacuYD2raSEuDXXUtfF7lEJN5BH/view?usp=sharing)
51+
52+
-**[WiL 2025](https://sites.google.com/view/wil2025/home)** – 9th Women in Logic Workshop <br/>
53+
14 July, Birmingham (United Kingdom). <br/>
54+
[Slides (PDF)](https://drive.google.com/file/d/1IU-zT0WePrNoYwhJFGfrahLi9APRbBOj/view)
55+
56+
-**[ICTCS 2025](https://ictcs2025.unich.it/)** – 26th Italian Conference on Theoretical Computer Science <br/>
57+
September 10-12, Pescara (Italy).<br/>
58+
[Slides (PDF)](https://drive.google.com/file/d/1niJI42GMCgGP7TfGVUtcw_NiGb8cqtM4/view)
59+
60+
-**[Proof and Computation 2025](https://www.mathematik.uni-muenchen.de/~schwicht/pc25.php)** - 9th Proof and Computation Autumn School <br/>
61+
September 15-19, Herrsching am Ammersee (Deutschland). <br/>
62+
[Slides (PDF)](https://drive.google.com/file/d/1zW_XKooRUQB4VSnLRZtj7O4OL32e6L3U/view)
63+
64+
##Evolution of HOLMS
65+
66+
**Modal Logics Mechanised in HOLMS** (chronological):
67+
68+
| Reference| Modal Logics|
69+
|-------------------------------|----------------------------|
70+
|**Journal of Automated Reasoning 63 (2023)**| GL|
71+
|**OVERLAY 2024 (2024)**| GL, K|
72+
|**Bilotta Master's Thesis (Spring 2025)**| GL, K, K4, T|
73+
|**WiL 2025, ICTCS 2025 (Summer 2025)**| GL, K, K4, T, S4, B, S5|
2174

2275
##Contributors
2376

24-
-[Antonella Bilotta](https://github.com/Antonella-Bilotta),University of Florence, Italy
77+
-[Antonella Bilotta](https://github.com/Antonella-Bilotta),Scuola Normale Superiore di Pisa, Italy
2578
-[Marco Maggesi](https://sites.google.com/unifi.it/maggesi/), University of Florence, Italy
2679
-[Cosimo Perini Brogi](https://logicosimo-gitlab-io-logicosimo-ad8371f8e99a5e895c64ff5b4f9ba89.gitlab.io/), IMT School for Advanced Studies Lucca, Italy
2780
- Leonardo Quartini, University of Florence, Italy
2881

2982

30-
##HOLMSUSAGE GUIDE
83+
##HOLMSUsage Guide
3184
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.
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+

0 commit comments

Comments
 (0)
[8]ページ先頭
©2009-2025 Movatter.jp