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 ofers 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.
Modal logic, a branch of formal logic that deals with possibility, knowledge, obligations, and many other
non-truth-functional constructs, is a powerful tool for reasoning about non-trivial scenarios in the real
world, computer science and AI [
Two of us have already developed a novel tool in the HOL Light proof assistant [20, 21] for automated proving and countermodel construction in Gödel-Löb logic (GL). In prior work [22, 23], we formalised a completeness proof of GL for its relational models, implementing both its axiomatic calculus and key aspects of possible-world semantics, such as a polymorphic bisimulation lemma. Furthermore, the tool provides a shallow embedding of a labelled sequent calculus for GL, automating proof search through a new HOL Light tactic applying the sequent rules guided by the syntactic structure of the modal formula under scrutiny stated as a HOL Light verification goal. The proof search either results in a theorem about provability in GL or identifies a countermodel to the input formula, extending
HOL Light’s capabilities to verify (modal counterparts of) central properties of mathematical theories extending Peano arithmetic [24]. Figure 1 summarises the overall procedure behind our implementation and the mathematically most relevant contents of the associated library.
Axiomat i↑c calculus ← Decision↓ procedure ←
Labelled sequent calculus ↖
↘ Irreflexive tr a→nsitive finite frames
The current status of the modal library GL in the oficial HOL Light repository covers Gödel-Löb logic
only.1 Nevertheless, our method is not per se limited to that specific modal system. The implementation
of a decision procedure via proof-search in labelled calculi based on formalised completeness results may
follow the general procedure of Figure 1 for any system in the modal cube [
The implementation we are introducing here goes precisely in that direction: to experiment with the flexibility of our original approach to the mechanisation of GL by considering, for a start, the modal cube, parametrising as far as possible the already developed code for Gödel-Löb logic to port it into a general framework for normal modal logic. This goal requires, first, to generalise our previous formalisation to the minimal system in the cube, namely the modal logic K, which characterises the whole class of relational frames.
It is with this spirit that, in the following pages, we survey the current status of HOLMS,2 our in-progress “HOL Light Library for Modal Systems”,3 aiming at endowing the HOL Light proof assistant with a general mechanism of automated theorem proving and countermodel construction for modal logics.4 Paper contents. We start by generalising the previously formalised notion of derivability in the axiomatic calculus for GL to a ternary deducibility relation ⊢ between a set of axiom schemas , a set of hypotheses ℋ, and a formula (Sect. 2.1).5 Next, moving to the semantic side, we re-use the basics of relational frames developed for the GL library (Sect. 2.2). By parametrising on the set the notion of relational frame, we can carry out the formal proof of completeness for K and GL in a uniform way, closer to the informal exposition given by e.g. [24], identifying the three key steps in the 1Our library is freely accessible from the oficial HOL Light distribution. 2HOLMS code is archived on Software Heritage. 3HOLMS documentation website https://holms-lib.github.io/. 4HOLMS code repository: https://github.com/HOLMS-lib/HOLMS. 5The set of schemas involved in such a relation is, ideally, any combination of axioms leading to a consistent modal system; for the present paper, we have restricted to K and GL only. general proof strategy for a broad class of extensions of K (Sect. 2.3). Since completeness holds for the appropriate classes of finite frames, decidability of K and GL follows (Sect. 2.4). Finally, we recap the shallow embedding of the labelled sequent calculus at the basis of the HOL Light decision procedure for the logics we are considering here, pointing to simple examples in the library of automated theorem proving and countermodel construction (Sect. 2.5).
All main statements reported in this document are hyperlinked with the corresponding snippet of code which the icon points to.
Related and future work. HOLMS is still at a rather embryo stage. Nevertheless, the methodology underlying our library is promising for eficiently using the formal infrastructure provided by the HOL Light proof assistant, which guarantees the (potentially) highest level of correctness of HOLMS and the automated reasoning we are implementing there. In future work, we plan to extend the library both concerning its dimensions (covering the whole modal cube, as well as modal systems beyond it, such as provability logics [25, 26, 27], intuitionistic/constructive modal logics [28, 29, 30, 31, 32, 33, 34], and many-dimensional modal logics [35, 36, 37, 38]) and its performance in verified proof search, improving the eficiency of our HOL Light tactic implementing the verification of modal statements and comparing it to standard benchmarks and diferent implementation paradigms [39, 40, 18, 41]. 6
.ℋ ⊢ is then inductively defined as follows.
After defining the basic syntax of the standard modal language, we formalise in HOL Light the notion of derivability of a formula from a set of hypotheses ℋ within a classical axiomatic calculus characterised by the modal schemas . We denote this relation with the expression .ℋ ⊢ .
As mentioned, the minimal logical engine we consider here consists of the standard axiomatisation of modal logic K, obtained from any classical propositional calculus by adding the schema K := □ ( → ) → (□ → □ ) and the necessitation rule .∅ ⊢ . The general relation .∅ ⊢ □ Definition 1 ( ). The ternary predicate .ℋ ⊢ , which denotes the derivability of a formula from a set of hypotheses ℋ in an axiomatic extension of logic K via schemas in the set , is inductively defined by the following conditions: • For every instance of axiom schemas for the calculus K, .ℋ ⊢ ; • For every ∈ ℋ, .ℋ ⊢ ; • For every instance of schemas in , .ℋ ⊢ ; • If .ℋ ⊢ → and .ℋ ⊢ , then .ℋ ⊢ ; • If .∅ ⊢ , then .ℋ ⊢ □ for any set of formulas ℋ.
In the following, we shall assume = ∅ or {GL}, where GL := □ (□ → ) → □ is the Gödel-Löb schema. It is easy to prove the deduction theorem for this notion of derivability from hypotheses. Theorem 1 (Deduction theorem
). For any , ℋ, , , the following equivalence holds: .ℋ ∪ ⊢ if .ℋ ⊢ → . 6Refer to Renate Schmidt’s online list for an overview of automated theorem provers for classical modal logic.
On the semantic side, the current version of HOLMS contains the formalisation of basic notions of frames and relational models, which we report below for the sake of completeness. Definition 2 ( ). A relational model ℳ is a triple ⟨, , V⟩ composed of a non-empty set of “possible worlds”, a binary “accessibility” relation ⊆ × , and an evaluation function V : × Atm → {0, 1} associating to each ∈ and each atom of the settled modal language a truth-value V(, ) ∈ {0, 1}.
The forcing relation ⊩ between a model ℳ = ⟨, , ⟩, a world ∈ , and a formula is inductively defined on the structure of as follows: • ⊩ ℳ ⇐⇒ V(, ) = 1, • ⊮ ℳ ⊥ for any , ℳ, • ⊩ ℳ ∧ ⇐⇒ ⊩ ℳ and ⊩ ℳ • ⊩ ℳ □ ⇐⇒ ∀ ∈ , if , then ⊩ ℳ .7 In words, when ⊩ ℳ , we say that “ is forced by in ℳ”.
When every world in ℳ forces a formula , we write ℳ ⊨ .
A formula is valid in a frame ℱ if it is true in any model based on that frame, i.e., if any world forces it for any evaluation function on ℱ . Formally, we write ⊨ ℱ if ⊨ ℳ for any ℳ based on ℱ .
A formula is valid in a class of frames S if is valid in any frame belonging to S. Formally, we write ⊨ S if ⊨ ℱ for any frame ℱ ∈ S.
The modal systems K and GL semantically coincide with the set of modal formulas valid in every frame K (K) and in every frame that is irreflexive, transitive, and finite ITF (GL), respectively. With the expressiveness of HOL Light, we can easily define such classes of frames and prove the soundness of the calculi we are considering: if .∅ ⊢ , then S ⊨ . From this result, the consistency ( , ) of these systems follows immediately: .∅ ̸⊢ ⊥.
It remains now to prove the other direction of the correspondence between the syntactic characterisation via ⊢ and the semantic characterisation via ⊨ of our systems, namely the formal proof of a completeness theorem for K and GL: if .∅ ̸⊢ , then there exists a model ℳ in the class S appropriate to such that ℳ ̸⊨ . Following the strategy outlined by [24], we note that it is possible to identify an informal line of reasoning common to the completeness proofs for K for K and for GL for ITF. Both proofs essentially follow three steps: 1. The identification of a non-empty set of possible worlds, given by a subclass of maximal consistent sets of formulas MAX , depending on and ; 2. The definition of a “standard” accessibility relation between these worlds such that the frame ⟨MAX , ⟩ is appropriate to ; 3. The reduction of the notion of forcing ⊩ to that of set-theoretic membership ∈ for every subformula of , through a specific atomic evaluation function on ⟨MAX , ⟩.
By working with the proof assistant, it is possible to identify all those lines of reasoning that are parametric for and develop each of the three steps while avoiding code duplication as much as possible. In particular, step 3 is already fully formalised in HOLMS within the following parametric truth lemma.8 7The remaining truth-functional operators are defined as usual in terms of ⊥ and ∧; similarly, we define the diamond operator 8Tashe◇ de:fin=iti¬ons of MAX and difer between K and GL, and in the current version of our library, they are encoded as two □ ¬ . distinct formal definitions.
Lemma 1 (Truth lemma ). Given such that .∅ ̸⊢ , and given the frame ⟨MAX , ⟩ which satisfies conditions 1-2 above, for every ∈ MAX and every subformula of , the following equivalence holds: ⊩ ⟨MAX,,ev ⟩ if ∈ , where ev (, ) := 1 if and only if is a subformula of and ∈ .
The availability of the parametric truth lemma is thus essential to formalise and prove the completeness theorem: Theorem 2 (Completeness , ). For every formula , if S ⊨ , then .∅ ⊢ .9
The formalisation of Theorem 2 ofers a valuable byproduct for automated reasoning. For verifying whether a formula of size is a theorem in a modal system , can be model-checked on all -models of size , for any ≤ 2. A basic approach involves applying the completeness theorem for finite frames, unfolding definitions, and solving the resulting semantic problem using first-order reasoning. This simple method can verify some lemmas in normal modal logics with non-trivial proofs in the axiomatic setting, and a more advanced implementation could add an OCaml function to bound frame sizes to improve its performance.
In HOLMS, instead of replicating these model-checking verification mechanisms, the approach focuses on logical verification through proof search, leveraging HOL Light’s goal-stack mechanism. Verifying a formula is reduced to constructing a formal derivation of the sequent ⇒ : in the labelled calculus for modal logic (K or GL). This construction is done via a shallow embedding, using labelled sequent calculus as a syntactic representation of relational semantics:
Semantic notation Labelled sequent calculus notation HOL Light notation ⊩ : holds (W,R) V A x
Notice that in holds (W,R) V A x the items W, R, V are made explicit as the components of the relational model on which the semantic forcing relation ⊨ is defined.
The goal-stack mechanism and forcing formalisation in HOL Light are thus adapted to develop proofs without formalising the entire calculus: we recall here the main lines of the implementation.10 Let us call any expression of forcing in HOL Light notation a holds-proposition.
HOL Light’s proof development is based on a single-consequent sequent calculus for higher-order logic. However, we need to extend this to a multi-consequent sequent calculus with lists of holdspropositions and relational atoms. To formalise commas, meta-level conjunction ’/\’ is used in the antecedent, and meta-level disjunction ’\/’ is used in the consequent. The basic workhorse tactics need to operate on two parts: (a) the goal term, corresponding to labelled formulas on the right of a sequent, and (b) the hypotheses list, corresponding to labelled formulas and relational atoms on the left. These tactics mimic traditional labelled calculus rules, providing the basic shallow embedding of the labelled system.
To automate proof search in this shallow-embedded calculus, two tactics (for GL and K ) are defined by following a root-first strategy in labelled sequent calculi. The process involves: 1. Setting the verification goal for a given modal formula in terms of derivability .∅ ⊢ ; 9We note in passing that although the class of frames S is polymorphic, the proof of the completeness theorem proceeds through a formal construction that restricts the result to the domain form list. However, the more general version of completeness is easily obtained through the formalisation of a type-theoretic version of the well-known bisimulation lemma, detailed in [23, § 4.4]. 10A detailed description of this adaptation is given in [23, § 6.2].
2. Introducing a model and world, reducing the goal to a holds-proposition, by applying the formal counterpart of Theorem 2; 3. Adding semantic hypotheses to handle modal and relational rules (e.g., transitivity for GL); 4. Applying propositional rules, prioritising non-branching ones, and the left rule for the modality, possibly reordering goal terms before triggering the rule for the modal operator on the right side of sequents, which are kept in specific normal form to facilitate the activation of the appropriate rules.
Steps 2-4 are repeated unless the same holds-proposition appears in both the hypotheses and disjuncts, in which case the branch closes successfully. Otherwise, when no rule can be triggered, the proof terminates with a countermodel, which the proof assistant displays to the user. If all branches and sub-goals are closed, the proof assistant returns a new HOL Light theorem stating that the input formula is a lemma of the modal system under consideration.
This work was partially funded by: the project SERICS – Security and Rights in CyberSpace PE0000014, ifnanced within PNRR, M4C2 I.1.3, funded by the European Union - NextGenerationEU (MUR Code: 2022CY2J5S); Istituto Nazionale di Alta Matematica – INdAM group GNSAGA. [11] E. Clarke, O. Grumberg, D. Peled, D. Peled, Model Checking, The Cyber-Physical Systems Series,
MIT Press, 1999. [12] A. S. Troelstra, H. Schwichtenberg, Basic proof theory, Second Edition, volume 43 of Cambridge tracts in theoretical computer science, Cambridge University Press, 2000. [13] A. Indrzejczak, Sequents and trees, Studies in Universal Logic, Birkhäuser, Cham (2021). [14] S. Negri, J. von Plato, Proof analysis: a contribution to Hilbert’s last problem, Cambridge University
Press, 2011. [15] T. Dalmonte, S. Negri, N. Olivetti, G. L. Pozzato, Theorem Proving for Non-normal Modal Logics, in: OVERLAY 2020, Udine, Italy, 2021. URL: https://hal.archives-ouvertes.fr/hal-03159954. [16] N. Olivetti, G. L. Pozzato, NESCOND: an implementation of nested sequent calculi for conditional logics, in: International Joint Conference on Automated Reasoning, Springer, 2014, pp. 511–518. [17] M. Girlando, B. Lellmann, N. Olivetti, G. L. Pozzato, Q. Vitalis, VINTE: an implementation of internal calculi for Lewis’ logics of counterfactual reasoning, in: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Springer, 2017, pp. 149–159. [18] M. Girlando, L. Straßburger, Moin: A nested sequent theorem prover for intuitionistic modal logics (system description), in: International Joint Conference on Automated Reasoning, Springer, 2020, pp. 398–407. [19] M. Girlando, B. Lellmann, N. Olivetti, S. Pesce, G. L. Pozzato, Calculi, countermodel generation and theorem prover for strong logics of counterfactual reasoning, Journal of Logic and Computation (2022). URL: https://doi.org/10.1093/logcom/exab084. doi:10.1093/logcom/exab084, exab084. [20] J. Harrison, The HOL Light Theorem Prover, Oficial webpage: https://hol-light.github.io/, 2024. [21] J. Harrison, HOL Light tutorial, http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf, 2017. [22] M. Maggesi, C. Perini Brogi, A Formal Proof of Modal Completeness for Provability Logic, in: L. Cohen, C. Kaliszyk (Eds.), 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2021, pp. 26:1–26:18. URL: https://drops. dagstuhl.de/opus/volltexte/2021/13921. doi:10.4230/LIPIcs.ITP.2021.26. [23] M. Maggesi, C. Perini Brogi, Mechanising Gödel-Löb Provability Logic in HOL Light, J.
Autom. Reason. 67 (2023) 29. URL: https://doi.org/10.1007/s10817-023-09677-z. doi:10.1007/ S10817-023-09677-Z. [24] G. Boolos, The logic of provability, Cambridge University Press, 1995. [25] R. L. Verbrugge, Provability Logic, in: E. N. Zalta, U. Nodelman (Eds.), The Stanford Encyclopedia of Philosophy, Summer 2024 ed., Metaphysics Research Lab, Stanford University, 2024. [26] G. Japaridze, D. De Jongh, The logic of provability, in: Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics, volume 137, Elsevier, 1998, pp. 475–546. [27] A. Das, I. van der Giessen, S. Marin, Intuitionistic Gödel-Löb logic, à la Simpson: labelled systems and birelational semantics, 2023. URL: https://arxiv.org/abs/2309.00532. arXiv:2309.00532. [28] A. K. Simpson, The Proof Theory and Semantics of Intuitionistic Modal Logic, PhD thesis,
University of Edinburgh. College of Science and Engineering. School of Informatics (1994). [29] S. Marin, M. Morales, L. Straßburger, A fully labelled proof system for intuitionistic modal logics, J. Log. Comput. 31 (2021) 998–1022. URL: https://doi.org/10.1093/logcom/exab020. doi:10.1093/ LOGCOM/EXAB020. [30] T. Litak, Constructive modalities with provability smack, in: Leo Esakia on duality in modal and intuitionistic logics, Springer, 2014, pp. 187–216. [31] S. Artemov, T. Protopopescu, Intuitionistic epistemic logic, The Review of Symbolic Logic 9.2 (2016) 266–298. [32] C. Perini Brogi, Curry–Howard–Lambek correspondence for intuitionistic belief, Studia Logica 109 (2021) 1441–1461. [33] G. Plotkin, C. Stirling, A framework for intuitionistic modal logics, in: Proceedings of the 1st
Conference on Theoretical Aspects of Reasoning about Knowledge (TARK), 1986, pp. 399–406. [34] A. Das, S. Marin, On intuitionistic diamonds (and lack thereof), in: International Conference on
Automated Reasoning with Analytic Tableaux and Related Methods, Springer, 2023, pp. 283–301. [35] A. Kurucz, F. Wolter, M. Zakharyaschev, D. M. Gabbay, Many-dimensional modal logics: theory and applications, Elsevier, 2003. [36] A. K. Simpson, Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS, J. Log. Algebraic Methods Program. 60-61 (2004) 287–322. URL: https://doi.org/10.1016/j. jlap.2004.03.004. doi:10.1016/J.JLAP.2004.03.004. [37] C. Perini Brogi, R. De Nicola, O. Inverso, Simpson’s proof systems for process verification: A ifne-tuning, in: Proceedings of the 25th Italian Conference on Theoretical Computer Science (ICTCS 2024), Turin, Italy, September 11-13, 2024, CEUR Workshop Proceedings, CEUR-WS.org, 2024. In print, Pre-proceedings online. [38] S. Docherty, R. N. Rowe, A non-wellfounded, labelled proof system for propositional dynamic logic, in: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Springer, 2019, pp. 335–352. [39] C. Nalon, U. Hustadt, F. Papacchini, C. Dixon, Local reductions for the modal cube, in: International Joint Conference on Automated Reasoning, Springer International Publishing Cham, 2022, pp. 486–505. [40] R. Goré, C. Kikkert, CEGAR-Tableaux: Improved Modal Satisfiability via Modal Clause-Learning and SAT, in: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Springer, 2021, pp. 74–91. [41] R. Goré, J. Kelly, Automated proof search in Gödel-Löb provability logic, in: abstract, British Logic
Colloquium, 2007. [42] A. Baanen, A. Bentkamp, J. Blanchette, J. Hölzl, J. Limperg, The Hitchhiker’s Guide to Logical
Verification, 2024. [43] L. Viganò, Labelled non-classical logics, Springer Science & Business Media, 2013.