HOLMS

A HOL Light Library for Modal Systems

This website gives a brief overview of our HOLMS library for the HOL Light theorem prover.

Publications

• 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.
  (In preparation)

Contributors

• 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

HOLMS USAGE GUIDE

The README.md provides a usage guide for our HOLMS library at its current status.

This site is open source. Improve this page.