📚 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 B1, Reading B1, Writing A2, Speaking A2

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, T, B, S4, S5, and GL, and we are working on on further extensions of 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, which I presented at ICTCS 2025;
- An extended paper describing the whole framework and introducing certified countermodels, accepted at CSL 26.

A. Bilotta, M. Maggesi, C. Pierini Brogi, 2026, "A modular framework for proof-search via formalised modal completeness in HOL Light", Accepted at CSL 2026, To appear.

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, 2025, "Growing a Modular Framewok for Modal Systems: HOLMS", Book of Abstract of Women in Logic 2025, pp. 7-11.

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.

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 reflection on the role of theorem provers in the context of mathematical knowldedge.
 

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.
 

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.

Note: Below is a list of conferences, summer schools, and workshops I have attended. Events where I presented a paper or talk are marked with an asterisk (*), and the slides for these presentations are attached to the corresponding asterisk.