📚 PhD Student in Logic at Scuola Normale Superiore di Pisa.
🎯 Code Developer and one of the main contributors of the HOLMS Framework.
📄 Here you can find my long CV, my SNS institutional webpage, my DBLP webpage and my Google Scholar webpage.

✨ More than anything, I would define myself as a curious person, always seeking new instruments to understand the world and the
human way of interpreting it.

🇮🇹 Italian: Mother tongue

🇬🇧 English: Listening C2, Reading C2, Writing C1, Speaking C1
Certified by IELTS (TRF: 25IT502528BILA010A) obtained on 24/04/2025.

🇫🇷 French: Listening B2, Reading B2, Writing B1, Speaking B1

My proposed PhD project aims to further extend this work, by mechanising additional modal logics (e.g. provability and intuitionistic logics) and developing a proof-theoretic analysis within the framework. I also intend to investigate various sequent calculi for modal logics, and to deepen my philosophical and technical reflection on the role of theorem provers and their integrations with LLMs (autoformalisation and self-learning loops) in mathematical practice.
 

Main Subjects Covered
I took courses in logic, as well as in philosophy of mathematics, history of logic, and general, corpus and computational linguistics.
In particular, I focused on Interactive Theorem Provers, Modal Logics, SAT/SMT Solvers, Proof Theory, Lambda Calculus, Computability Theory, Model Theory and Quantum Computing.

Research and Contributions
After completing my exams, I joined the HOLMS research project on the mechanisation of modal logics within HOL Light proof assistant.
My Master's thesis extended the first version of HOLMS by modularising the existing code and implementing three additional logics.
 

I initially studied various branches of philosophy, as well as logic and history.
I then focused my studies on philosophy of mathematics, philosophy of science, and mathematical logic.
Additionally, I took extra courses in the Department of Mathematics, including: algebra 1, analysis 1, computer science (C++) and foundations of mathematics. This multidisciplinary approach enabled me to write a thesis exploring the formalist perspective and Hilbert’s contributions to the foundations and philosophy of mathematics.
 

Since its beginnings, I have been part of the HOLMS research project , which focuses on the mechanisation of modal logics with the aid of interactive theorem provers. HOLMS library currently provide the mechanisation of the normal modal logics K, K4, D, T, B, S4, S5, and GL, toghether with Grz implemented via modal translations. We aim to further extend the framework by mechanising additional modal logics (e.g., provability and intuitionistic logics), experimenting with different mechanisation techniques (e.g., modal translations), and developing a proof-theoretic analysis within the framework.

As part of this project, I developed my Master’s thesis, contributed to code and website development, and co-authored the following papers:
- A communication paper introducing the first version of HOLMS at OVERLAY 2024;
- A long abstract outilining some implementation features of the framework, presented at Women in Logic 2025;
- A communication paper reporting the results of my thesis and completeness proofs for additional logics, presented at ICTCS 2025;
- An extended paper describing the whole framework and introducing certified countermodels, presented at CSL 26;
- An extended paper experimenting with modal translations and implementing Grz, accepted at IJCAR 26.

A. Bilotta, M. Maggesi, C. Pierini Brogi, 2026, "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).

A. Bilotta, M. Maggesi, C. Pierini Brogi, 2026, "A modular framework for proof-search via formalised modal completeness in HOL Light", Proceedings of the 34th EACSL Annual Conference on Computer Science Logic (CSL 26), Volume 363 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 18:1–18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

A. Bilotta, M. Maggesi, C. Pierini Brogi, 2025, "A modular proof of semantic completeness for normal systems beyond the modal cube, formalised in HOLMS", Proceedings of the 26th Italian Conference on Theoretical Computer Science, ICTCS 2025, volume 4039 of CEUR Workshop Proceedings, pp. 154-162 .

A. Bilotta, M. Maggesi, C. Pierini Brogi, L. Quartini, 2024, "Growing HOLMS, a HOL Light Library for Modal Systems", Short Paper Proceedings of the 6th International Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, OVERLAY 2024, volume 3904 of CEUR Workshop Proceedings, pp. 41–48.

A. Bilotta, M. Maggesi, C. Pierini Brogi, 2026, "Growing HOLMS: Grzegorczyk Logic and Experiments with Translations in HOL Light", Book of Abstract of Women in Logic 2026

A. Bilotta, M. Maggesi, C. Pierini Brogi, 2025, "Growing a Modular Framewok for Modal Systems: HOLMS", Book of Abstract of Women in Logic 2025, pp. 7-11.

Note: Slides for these presentations are attached to the asterisk.

Member of the European Association for Computer Science Logic (EACSL).

Member of the European Association for Theoretical Computer Science (EATCS) and of its Italian Chapter.

Member of the EC-COST Action (CA20111) European research network on formal proof (EuroProofNet).
Member of the Working Groups ATPs, Program verification, Libraries of formal proofs.
Selected for in-person participation (with reimbursement) in the EuroProofNet School on Natural Formal Mathematics, June 2025, Bonn, Germany.

Popularisation project for middle-school students to promote the participation of women in science, organised by Scuola Normale.

Participation in the organisation of four seminars on science and literature, funded by the University of Florence.