Shared Libraries
- A simple checker for boolean tautologies
- A slightly more powerful done tactic
- Generic Lemmas not in Ssreflect
- Finite Sets over choice types and countable types
- Automation for finite Sets
- Induced Symmetric Subrelations
- A Modular Library for Reasoing in Hilbert Systems
- Generic Lemmas for Literals and Support
Basic Modal Logic K
- K in Coq
- Hilbert System
- Signed Formulas, Clauses, and Support
- Demos
- Hilbert Refutations
- Gentzen System for K
- Construction of a Universal Model
- Main Results
Modal Logic with Transitive Closure
- K* in Coq
- Hilbert System
- Clauses and Support
- Demos
- Hilbert Refutations
- History-based Gentzen system for K*
- Main Results
Computation Tree Logic
- CTL in Coq
- Clauses and Support
- Hilbert System for CTL
- Directed Acyclic Graphs
- Relaxed Demos
- Model Construction
- Pruning
- Completeness of the Hilbert system
- Emerson's Axiomatization
- Axiomatization of Lange and Stirling
- Agreement of Paths Semantics and Inductive Semantics
- 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
- Decidability of Gentzen Derivability
- Main Results