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.
</i><a href="http://www.ps.uni-saarland.de/extras/itp14">Coq Development</a><i>