We communicate here the most recent extension of HOLMS, our library for modal logics aimed at introducing automated modal reasoning within the HOL Light proof assistant. Based on a uniform proof strategy, we present a more refined formal proof of completeness for systems within and beyond the S5-normal modal cube, notably Gödel-Löb logic. We report on our development by adopting a measure of its modularity based on Strachey's distinction between parametric and ad hoc polymorphic code.
A Modular Proof of Semantic Completeness for Normal Systems beyond the Modal Cube, Formalised in HOLMS / Bilotta A.; Maggesi M.; Perini Brogi C.. - ELETTRONICO. - 4039:(2025), pp. 154-162. ( 26th Italian Conference on Theoretical Computer Science, ICTCS 2025 Campus of Pescara, at the Department of Economic Studies of the University of Chieti-Pescara, ita 2025).
A Modular Proof of Semantic Completeness for Normal Systems beyond the Modal Cube, Formalised in HOLMS
Maggesi M.;Perini Brogi C.
2025
Abstract
We communicate here the most recent extension of HOLMS, our library for modal logics aimed at introducing automated modal reasoning within the HOL Light proof assistant. Based on a uniform proof strategy, we present a more refined formal proof of completeness for systems within and beyond the S5-normal modal cube, notably Gödel-Löb logic. We report on our development by adopting a measure of its modularity based on Strachey's distinction between parametric and ad hoc polymorphic code.
| File | Dimensione | Formato | |
|---|---|---|---|
|
Bilotta, Maggesi, Brogi (2025) HOLMS.pdf
accesso aperto
Descrizione: Copia della versione disponibile da CEUR-WS
Tipologia:
Pdf editoriale (Version of record)
Licenza:
Creative commons
Dimensione
310.3 kB
Formato
Adobe PDF
|
310.3 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
