We prove completeness and decidability results for the temporal logic CTL in Coq/Ssreflect. Our basic result is a constructive proof that for every formula one can obtain either a finite model satisfying the formula or a proof in a Hilbert system certifying the unsatisfiability of the formula. The proof is based on a history-augmented tableau system obtained as the dual of Brünnler and Lange's cut-free sequent calculus for CTL. We prove the completeness of the tableau system and give a translation of tableau refutations into Hilbert refutations. Decidability of CTL and completeness of the Hilbert system follow as corollaries. © 2014 Springer International Publishing.
CITATION STYLE
Doczkal, C., & Smolka, G. (2014). Completeness and decidability results for CTL in Coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8558 LNCS, pp. 226–241). Springer Verlag. https://doi.org/10.1007/978-3-319-08970-6_15
Mendeley helps you to discover research relevant for your work.