KM.Algebra.KMH_alg_completeness

• Completeness of KM w.r.t. algebraic semantic

KM.Algebra.KMH_algebraizable

• Algebraisability of KM

KM.Algebra.KMH_implicative

• Implicativity of KM

KM.Algebra.KM_Algebras

• Algebras for KM
• Properties of KM-algebras

KM.Algebra.alg_soundness

• Soundness of KM w.r.t. algebraic semantics

KM.Algebra.algebraic_semantic

• Algebraic semantic over KM-algebras

KM.GHC.KMH

KM.GHC.KMH_export

KM.GHC.Lindenbaum_lem

KM.GHC.enum

KM.GHC.logics

KM.GHC.properties

KM.GHC.same_calcs

KM.Kripke.kripke_export

KM.Kripke.kripke_sem

KM.Kripke.soundness

KM.Sequent.Cut

• Cut Admissibility

KM.Sequent.DecisionProcedure

• Decision Procedure

KM.Sequent.Environments

• Environments
  • Multiset utilities
  • Conjunction, disjunction, and implication
  • A dependent version of `map`
  • Tactics

KM.Sequent.Equiv_KMH

KM.Sequent.Optimizations

• Optimizations of formulas
  • Correctness of optimizations
  • Generalized rules

KM.Sequent.Order

• Ordering

KM.Sequent.PropQuantifiers

• Propositional Quantifiers
  • Definition of propositional quantifiers.
  • Correctness
  • Main uniform interpolation Theorem

KM.Sequent.SequentProps

• Admissible rules in G4KM sequent calculus
  • Weakening
  • Inversion rules
  • Contraction on the left and on the right.
  • Admissibility of the implication left rule

KM.Sequent.Sequents

• Sequent calculus G4KM
  • Definition of provability in G4KM
  • Tactics

KM.Sequent.Simp_env

• Simplifications for formulas and contexts
  • Applicability of rules
  • Ternary if notation
  • Definition of contextual simplification
  • Weight lemmas
  • Simplifying environments
• Simplification of a context as seen as a left-hand-side of a sequent
• Simplification of a context as seen as a right-hand-side of a sequent
  • Simplification and the weight ordering
  • Simplification is provably equivalent
  • Simplification does not introduce new variables

KM.Sequent.Simplifications

• Equivalence of environments, seen as conjunctions on the left of a sequent.
• Equivalence of environments, seen as disjunctions on the right of a sequent.

KM.Sequent.syntax_facts

• • Countability of the set of formulas
  • Weight of formulas

KM.Syntax.syntax

KM.extraction.Extraction