This paper reports on the formalization of classical hybrid logic with eventualities in the constructive type theory of the proof assistant Coq. We represent formulas and models and define satisfiability, validity, and equivalence of formulas. The representation yields the classical equivalences and does not require axioms. Our main results are an algorithmic proof of a small model theorem and the computational decidability of satisfiability, validity, and equivalence of formulas. We present our work in three steps: propositional logic, modal logic, and finally hybrid logic.
Paper, CPP 2011