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
  • 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
  • Pruning
    • Pruning yields a demo
    • Refutation Calculus
    • Refutation Completeness
  • Completeness of the Hilbert system
    • Pruning refutations to Hilbert Refutations
    • Informative Completeness and Corollaries
  • Emerson's Axiomatization
    • Completeness
    • Soundness
  • Axiomatization of Lange and Stirling
    • Completeness
    • 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
  • History-Based Gentzen System for CTL
  • Translation of History Rules to Hilbert Refutations
  • Translation from Gentzen derivations to Hilbert Refutations
  • Completeness of the Gentzen System
    • Pruning Refutations to Gentzen derivations
    • Completeness Theorem
  • Decidability of Gentzen Derivability
    • Part 1: Syntactic Universe
    • Part 2: Decidability inside a universe
    • Part 3: Existence of universes for all clauses
  • Main Results
Generated by coqdoc and improved with CoqdocJS