Growing HOLMS, a HOL Light Library for Modal Systems

This paper introduces HOLMS (HOL-Light Library for Modal Systems), a new framework within the HOL Light proof assistant, designed for automated theorem proving and countermodel construction in modal logics. Building on our prior work focused on Gödel-Löb logic (GL), we generalise our approach to cover a broader range of normal modal systems, starting here with the minimal system K. HOLMS provides a flexible mechanism for automating proof search and countermodel generation by leveraging labelled sequent calculi, interactive theorem proving, and formal completeness results. It thus offers the inception of a comprehensive tool for modal logic reasoning at a high level of confidence and automation. Our on-going HOLMS project aims to create a uniform, scalable method for handling multiple modal systems within HOL Light, thereby advancing the automation of modal reasoning within proof assistants.