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.
Browse the Sources (updated 10-07-2014)
Browse the Sources (proofs suppressed,updated 10-07-2014)
Coq development (tar archive, includes fset library,updated 10-07-2014)