Project Page Index Table of Contents Demo
  • Cut Admissibility
  • Decision Procedure
  • Environments
    • Multiset utilities
    • Conjunction, disjunction, and implication
    • A dependent version of `map`
    • Tactics
  • Formulas
    • Definitions and notations.
    • Countability of the set of formulas
    • Weight
  • Optimizations of formulas
    • Correctness of optimizations
    • Generalized rules
      • Generalized OrL and its invertibility
      • Generalized OrR
      • Generalized AndR
      • Generalized invertibility of AndR
      • Generalized AndL
  • Ordering
  • Propositional Quantifiers
    • Definition of propositional quantifiers.
    • Correctness
      • (i) Variables
      • (ii) Entailment
      • (iii) Uniformity
    • Main uniform interpolation Theorem
  • Admissible rules in G4ip sequent calculus
    • Weakening
    • Inversion rules
    • Contraction
    • Admissibility of LJ's implication left rule
  • Sequent calculus G4iSL
    • Definition of provability in G4iSL
    • Tactics
  • Simplifications for formulas and contexts
    • Applicability of rules
    • Ternary if notation
    • Definition of contextual simplification
    • Weight lemmas
    • Simplifying environments
    • Simplification and the weight ordering
    • Simplification is provably equivalent
    • Simplification does not introduce new variables
Generated by coqdoc and improved with CoqdocJS