Growing HOLMS: A Verified Automated Prover for Grzegorczyk Logic in HOL Light

This paper presents a certified theorem prover for Grzegorczyk logic (Grz) implemented in the general-purpose proof assistant HOL Light. Our prover builds on original HOL Light formalisations of modal adequacy for Grz with respect to finite partially ordered frames, and on the standard full and faithful translation of Grz into Gödel–Löb logic (GL). This formalised embedding allows us to extend the range of modal systems supported by the HOLMS library for automated modal reasoning, and constitutes a new methodology experimented in our framework, being the first logic added to the library through a modal translation.