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
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 in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
paper10.pdf
accesso aperto
Descrizione: AModular Proof of Semantic Completeness for Normal Systems beyond the Modal Cube, Formalised in HOLMS
Tipologia:
Versione Editoriale (PDF)
Licenza:
Creative commons
Dimensione
310.3 kB
Formato
Adobe PDF
|
310.3 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
