2026-07-23T20:14:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25442 2026-03-19T13:28:36Z ddc:004 open_access

A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light Bilotta, Antonella Maggesi, Marco Perini Brogi, Cosimo Modal logic HOL Light Labelled sequent calculi Logical verification Interactive theorem proving Automated proof-search We extend the existing HOL Light Library for Modal Systems (HOLMS) to support a modular implementation of modal reasoning within the HOL Light proof assistant. We deeply embed axiomatic calculi and relational semantics for seven normal modal logics (K, T, B, K4, S4, S5, GL) and formalise modal adequacy theorems for these systems. We then leverage those formalisations to implement a mechanism for automated reasoning via proof-search in the associated labelled sequent calculi, which we shallowly embed in HOL Light’s goal-stack mechanism. This way, we equip the general-purpose proof assistant with (semi)decision procedures for these logics that, in case of failure to construct a proof for the input formula, return a certified countermodel within the appropriate class for the logic under consideration. On the methodological side, we propose a precise measure of the modularity of our approach by systematically adopting Christopher Strachey’s distinction between ad hoc and parametric polymorphism throughout the library. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Antonella Bilotta and Marco Maggesi and Cosimo Perini Brogi 2026 Is Part Of LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2026.18 urn:nbn:de:0030-drops-254427 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.18 eng https://creativecommons.org/licenses/by/4.0/legalcode