Library tactics
Library base
Generic lemmas not in Ssreflect
Finitely branching Trees over countable Types
A least fixed point operator for finType
Library syntax
Syntax
A countType instance for formulas
Subformulas
Library hilbert
The Hilbert System for K+
Reasoning Infrastructure
Phase 1 - Combinators
Phase 2 - Rewriting with the entailment relation
Phase 3 - Assumption Management
Modal Logic Lemmas
Library models
Transition Systems
Transitive Closure
Satisfaction and Models
Finite Models
Library gentzen
Gentzen Systems as Decision Procedures
Signed formulas and clauses
Demos
Sequent System for K^+
Propositional Retracts
Jumps and Loops
Derivability
The Demo of underivable Clauses
Model Existence
Translation Theorem
Main Results
This page has been generated by
coqdoc