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.
2021
12th International Conference on Interactive Theorem Proving (ITP 2021)
12th International Conference on Interactive Theorem Proving (ITP 2021)
Italy, Rome (Virtual)
29 June – 01 July, 2021
Marco Maggesi; Cosimo Perini Brogi
File in questo prodotto:
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.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/1225580
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact