# Publication details

##
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

@INPROCEEDINGS{DoczkalSmolka:2014:comp-dec-CTL,
title = {Completeness and Decidability Results for CTL in Coq},
author = {Christian Doczkal and Gert Smolka},
year = {2014},
editor = {G. Klein and G. Gamboa},
publisher = {Springer},
booktitle = {Interactive Theorem Proving (ITP 2014)},
series = {LNAI},
volume = {8558},
pages = {226-241},
}

Login to edit

Webmaster,
Wed Sep 16 10:47:00 2009