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, Antonella
;
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 | |
|---|---|---|---|
|
ICTCS_2025_Camera_ready_10.pdf
accesso aperto
Tipologia:
Published version
Licenza:
Creative Commons
Dimensione
222.74 kB
Formato
Adobe PDF
|
222.74 kB | Adobe PDF |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
