Growing a Modular Framework for Modal Systems- HOLMS: a HOL Light Library

TL;DR

HOLMS is a modular HOL Light library that automates modal reasoning, proving adequacy theorems for various modal systems, and integrating decision procedures and countermodel generation within a proof assistant.

Contribution

This work introduces a unified, modular approach for proving adequacy theorems in HOL Light for multiple modal systems, extending previous research and integrating automated tools.

Findings

Successfully formalized adequacy theorems for K, T, K4, and GL.

Implemented automated decision procedures and countermodel constructors.

Demonstrated the feasibility of mechanizing modal reasoning in HOL Light.

Abstract

The present dissertation introduces the research project on HOLMS (\textbf{HOL} Light Library for \textbf{M}odal \textbf{S}ystems), a growing modular framework for modal reasoning within the HOL Light proof assistant. To provide an accessible introduction to the library, the fundamentals of modal logic are outlined first, followed by a concise manual for the proof assistant itself. The core contribution of this work on HOLMS is the development of a unified and modular strategy for proving adequacy theorems with respect to relational semantics directly within HOL Light for several normal modal systems, currently including K, T, K4, and GL. Adequacy theorems establish a formal connection between syntactic proof systems and their intended relational models, ensuring that derivable statements align with valid ones. This approach extends previous research on G\"odel-L\"ob logic (GL) by two HOLMS developers. It also assesses the generality and compositionality of the completeness proofs in George Boolos' monograph \textit{The logic of provability}. Beyond theoretical contributions, HOLMS incorporates automated decision procedures and a countermodel constructor for K, T, K4, and GL, illustrating how general-purpose proof assistants can be effectively combined with research on labelled sequent calculi and key insights from correspondence and bisimulation theories. The implementation in HOL Light demonstrates the feasibility of mechanising modal reasoning in a flexible and robust manner, paving the way for further developments of the HOLMS framework.