(c) Copyright, Marco Maggesi, Cosimo Perini Brogi 2020-2022.
This repository contains a formal proof of the modal completeness for the provability logic GL in HOL Light.
The top-level file is make.ml.
The main theorem is COMPLETENESS_THEOREM_GEN in file completeness.ml.