Reseña: Completeness and decidability results for CTL in Coq
Se ha publicado un artículo de razonamiento formalizado en Coq sobre metalógica titulado Completeness and decidability results for CTL in Coq.
Sus autores son Christian Doczkal y Gert Smolka (de la Saarland University, Saarbrücken).
Su resumen es
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.
El trabajo se presentará hoy en el ITP 2014 (5th Conference on Interactive Theorem Proving).
El código de las correspondientes teorías en Coq se encuentra aquí.