2 citations · 4 across the 5 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2022★ 2 cited
Mechanising Gödel-Löb provability logic in HOL Light
Marco Maggesi, Cosimo Perini Brogi
We introduce our implementation in HOL Light of the metatheory for Gödel-Löb provability logic (GL), covering soundness and completeness w.r.t. possible world semantics and featuri…
cs.LO2021★ 2 cited
A formal proof of modal completeness for provability logic
Marco Maggesi, Cosimo Perini Brogi
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 som…