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
Optimizing 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