Interacting with modal logics in the Coq proof assistant

Abstract

This paper describes an embedding of higher-order modal logics in the Coq proof assistant. Coq’s capabilities are used to implement modal logics in a minimalistic manner, which is nevertheless sufficient for the formalization of significant, non-trivial modal logic proofs. The elegance, flexibility and convenience of this approach, from a user perspective, are illustrated here with the successful formalization of Gödel’s ontological argument. Show more