Publication details
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
@INPROCEEDINGS{DoczkalSmolka:2011:Constructive:0,
title = {Constructive Formalization of Hybrid Logic with Eventualities},
author = {Christian Doczkal and Gert Smolka},
year = {2011},
month = {Dec},
editor = {Jean-Pierre Jouannaud, Zhong Shao},
publisher = {Springer},
booktitle = {Certified Programs and Proofs, First International Conference (CPP 2011)},
series = {LNCS},
volume = {7086},
pages = {5-20},
}
Login to edit
Legal notice, Privacy policy
