This work presents a formalized proof of modal completeness for Gödel-Löb provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation. In particular, we show how we adapted the proof in the Boolos' monograph according to the formal language and tools at hand. The strategy we develop here overcomes the technical difficulty due to the non-compactness of GL, and simplify the implementation. Moreover, it can be applied to other normal modal systems with minimal changes.
A formal proof of modal completeness for provability logic / Marco Maggesi; Cosimo Perini Brogi. - ELETTRONICO. - 193:(2021), pp. 1-18. (Intervento presentato al convegno 12th International Conference on Interactive Theorem Proving (ITP 2021) tenutosi a Italy, Rome (Virtual) nel 29 June – 01 July, 2021) [10.4230/LIPIcs.ITP.2021.26].
A formal proof of modal completeness for provability logic
Marco Maggesi;Cosimo Perini Brogi
2021
Abstract
This work presents a formalized proof of modal completeness for Gödel-Löb provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation. In particular, we show how we adapted the proof in the Boolos' monograph according to the formal language and tools at hand. The strategy we develop here overcomes the technical difficulty due to the non-compactness of GL, and simplify the implementation. Moreover, it can be applied to other normal modal systems with minimal changes.File | Dimensione | Formato | |
---|---|---|---|
2102.05945.pdf
accesso aperto
Descrizione: Versione ArXiv febbraio 2021
Tipologia:
Altro
Licenza:
Creative commons
Dimensione
570.46 kB
Formato
Adobe PDF
|
570.46 kB | Adobe PDF | |
LIPIcs-ITP-2021-26.pdf
accesso aperto
Descrizione: Versione disponibile online dall'editore.
Tipologia:
Pdf editoriale (Version of record)
Licenza:
Creative commons
Dimensione
715.63 kB
Formato
Adobe PDF
|
715.63 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.