Completeness and Decidability Results for CTL in Coq
Note: You can click on any defined object to look up its definition
CTL in Coq
Formulas
Models
Hilbert System
Finite Models
Signed Formulas
Subformula Closure
History-based Tableaux for CTL
Decidability of Tableau Derivability
Part 1: Syntactic Universe
Part 2 : Decidability inside a universe
Part 3: Existence of universes for all clauses
Demos
Demos to Models
Tableaux to Demos
A Modular Library for Reasoing in Hilbert Systems
Minimal Logic
Propositional Logic
Basic Modal Logic
CTL
Tableau Refutations to Hilbert Refutations
Associtated Formuals
Translation of History Rules
Translation Theorem
Infrastructure
Termination and Transitive Closure
Finite Rooted Labeled Graphs
Finitely Branching Trees and Conversion to Rooted Dags
Finite Sets over Choice- and Countable Types
This page has been generated by
coqdoc