Publication details

Saarland University Computer Science

Constructive Formalization of Hybrid Logic with Eventualities

Christian Doczkal, Gert Smolka

Certified Programs and Proofs, First International Conference (CPP 2011), Vol. 7086 of LNCS, pp. 5-20, Springer, December 2011

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.

Coq Development

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy