- Library enhancements
- Misc stuff
- Sets
- Lists
- some_nth predicate for lists
- Dependent lists
- Reordering of lists
- Lists as simple sets
- Lists as multisets
- Support of lists
- association lists
- A special some predicate for lists
- Basic definition for decidable sets
- Functions
- Direct and inverse image for functions
- Classical reasoning
- Coq casts for function domains and codomains and results
- Category theory
- Logic, basic definitions
- Formulas, Sequents, Proofs
- Lambda Formulas, page 5
- Utility functions for formulas
- Inversion lemmas for lf_modal
- Sequents, Rules
- simple propositional sequents
- Formula measure for different purposes
- Proofs
- Recursion for proofs
- Proof depth
- Induction on proofs
- Provability
- Interpretation of sequents, page 9
- Proof monotonicity (wrt. the rules and hypothesis)
- Provability is closed under reordering
- Make sequent multisets out of lists
- Plug proofs for hypothesis
- Provability with different rules
- Modal rank, page 5
- Rank of sequents
- Ranked sequent sets
- Ranked rules
- Minimal rank of a rule
- Minimal rank of proofs
- Extract the list of propositional variables
- Substitutions
- Propositional formulas and sequents
- Different subsets of formulas and sequents
- Renaming
- Various rules
- Rule sets
- Admissible rules
- Formulas Prop(Lambda(S)) or V
- Formulas, Sequents, Proofs
- Logic library
- Properties of coalgebraic logics, Section 3
- Results on propositional logic
- Semantics
- Standard Semantics
- Coalgebraic models
- Normative semantics
- Simplified sequence semantics
- Equivalence for simplified semantics
- Standard semantic lemma (derived via simplified semantics)
- Semantics X,tau |= f for propositional f
- Equivalence of standard semantics with X,tau |= f
- Simplified X,tau |= f sequent semantics
- Equivalence for simplified X,tau |= f sequent semantics
- Semantics TX,tau |= f for counted modal arguments
- Semantics TX,tau |= f for modal formulas f
- Equivalence of standard semantics with TX,tau |= f
- Simplified TX,tau |= f sequent semantics
- Equivalence for simplified TX,tau |= f sequent semantics
- One-step conditions, 4.1 - 4.3
- N-step semantics 4.9 - 4.10, 4.12
- Definition of n-step semantics, Def 4.9
- Lemma 4.10, relate n-step semantics to standard semantics
- Towards corollary 4.12
- Simplified n-step sequent semantics
- Correctness of simplified n-step sequent semantics
- Simplified n-step semantics validity and reorder lemmas
- Upward correctness of n-step semantics and context lemma
- Preservation of n-step validity in proof trees
- Relation to propositional models
- First projection for n-step semantics of prop_modal sequents
- Second projection of n-step semantics for propositional sequents
- Relation to prop_modal_prop semantics TX,tau |= f via substitution
- Relation to propositional semantics X,tau |= f via substitution
- Standard Semantics
- Completeness and semantic cut elimination, Section 4
- Syntactic cut elimination, Section 5
- K example
- Other material
- Import all
This page has been generated by coqdoc