Main Page
Index
Table of Contents
CTL in Coq
Inductive Characterizations
Path Characterizations
Formulas
Models
Satisfaction for inductuvice and path semantics
Finite Models
Clauses and Support
Signed Formulas
Clauses and Support
Request
Subformula Universes
Size
Hilbert System for CTL
Soundness
Agreement of Paths Semantics and Inductive Semantics
Agreement on Finite Models
Agreement on General Models
Soundness of Hilbert System for Path Semantics and General Models
Agreement with Disjunctive Release implies LPO
Directed Acyclic Graphs
Termination and Transitive Closure
Finite Rooted Labeled Graphs
Relaxed Demos
Relaxed Fulfillment
Fragment Demos
Model Construction
Relaxed Fullfillment to Fragments
Fragments to Models
Fulfillment relations
Pruning
Pruning yields a demo
Refutation Predicates and corefutability of the pruning demo
Hilbert Refutations
Main Results