This website gives a brief overview of our HOLMS library for the HOL Light theorem prover.
- Marco Maggesi, Cosimo Perini Brogi (2021)
A Formal Proof of Modal Completeness for Provability Logic.
In 12th International Conference on Interactive Theorem Proving (ITP 2021).
Leibniz International Proceedings in Informatics (LIPIcs),
Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
DOI:10.4230/LIPIcs.ITP.2021.26 (Open access) - Marco Maggesi, Cosimo Perini Brogi (2023)
Mechanising Gödel–Löb Provability Logic in HOL Light.
J Autom Reasoning 67, 29. DOI:10.1007/s10817-023-09677-z (Open access) - Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini (2024)
Growing HOLMS, a HOL Light Library for Modal Systems.
OVERLAY 2024 - 6th International Workshop on Intelligence and fOrmal VERification, Logic, Automata, and sYnthesis
28 and 29 November, Bolzano (Italy).
Download.
- Antonella Bilotta, University of Florence, Italy
- Marco Maggesi, University of Florence, Italy
- Cosimo Perini Brogi, IMT School for Advanced Studies Lucca, Italy
- Leonardo Quartini, University of Florence, Italy
The README.md provides a usage guide for our HOLMS library at its current status.