Growing HOLMS: a modular framework for modal logics within HOL Light Proof Assistant

This talk introduces HOLMS (HOL Light Library for Modal Systems), a framework designed for formalising and implementing a variety of modal logics. We present the latest developments of the library, which currently provides uniform formalisations—via axiomatic calculi, semantics, and labelled sequent calculi—alongside certified automated theorem proving for nine normal modal systems. Seven of these logics (K, D, T, B, K4, S4, and S5) belong to the modal cube and are implemented using a highly modular strategy. The library also covers Gödel-Löb logic (GL) and Grzegorczyk logic (Grz). For the latter, we explore a novel implementation strategy via modal translation: by embedding Grz into GL, we leverage the existing mechanisation of GL to provide automated support for Grzegorczyk logic.