Publication details

Saarland University Computer Science

Completeness and Decidability Results for CTL in Coq

Christian Doczkal, Gert Smolka

Interactive Theorem Proving (ITP 2014), Vol. 8558 of LNAI, pp. 226-241, Springer, 2014

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.

Coq Development

Download PDF        Show BibTeX               

Login to edit

Webmaster, Wed Sep 16 10:47:00 2009