+
+
+
+
+
+General
+-
+
- Existential quantifiers in Type + + +
- General purpose tools in Type + + +
- Constructions for inductive proofs about derivations (1) + + +
- Constructions for inductive proofs about derivations (2) + + +
- Lemmas about lists in Type + + +
- Reflexive transitive closure, in Type + + +
- Strong induction on natural numbers + + +
- Definition of swapped, and lemmas + + +
- Derivations in Type + + +
- General elements about sequents + + +
- General tactics + + +
- General tools + + +
- Derivations as data structures + + +
- Insertions of elements in a list + + +
- Modifications of elements in a list + + +
- Export file for General + + +
Syntax for K and GL
+-
+
- Definition of formulas + + +
- Lemmas about lists of formulas + + +
- Lemmas about removing elements from lists of formulas + + +
- Export file for Syntax + + +
The calculus KS and its properties
+-
+
- Definition of KS + + +
- Decidability of the application of rules + + +
- Admissibility of exchange
+
-
+
- Preliminaries + + +
- ImpR rule + + +
- ImpL rule + + +
- KR rule + + +
- Admissibility + + +
+
+ - Termination of the naive strategy
+
-
+
- Definition of measure + + +
- Preliminaries + + +
- Initial rules + + +
- ImpR rule + + +
- ImpL rule + + +
- KR rule + + +
- Termination + + +
+ - Admissibility of weakening + + +
- Invertibility of ImpR and ImpL + + +
- Admissibility of contraction + + +
- Admissibility of cut + + +
- Elimination of cut + + +
- Export file for KS + + +
Uniform interpolation for K
+-
+
- Craig interpolation + + +
- Irreducibility function
+
-
+
- Definition + + +
- Specifications + + +
+ - Lexicographic order + + +
- Definition canopy + + +
- Definition of the uniform interpolant function via the Braga method + + +
- Preliminaries + + +
- Basics + + +
- Correctness
+
-
+
- Variables + + +
- Entailment + + +
- Uniformity + + +
+
The calculus GLS and its properties
+-
+
- Definition of GLS + + +
- Decidability of the application of rules + + +
- Admissibility of exchange + + + +
- Termination of the naive strategy
+
-
+
- Shortlex order + + +
- Definition of measure and termination + + +
+ - Admissibility of weakening + + +
- Invertibility of ImpR and ImpL + + +
- Admissibility of contraction + + +
- Admissibility of cut + + +
- Elimination of cut + + +
- Decidability of provability + + +
- Export file for GLS + + +
Uniform interpolation for GL
+-
+
- Craig interpolation + + +
- Irreducibility function
+
-
+
- Definition + + +
- Specifications + + +
+ - Ordering sequents
+
-
+
- Lexicographic order + + +
- Order on sequents + + +
+ - Definition of contracted sequents + + +
- Permutations + + +
- Canopy
+
-
+
- Definition canopy + + +
- Canopy and ImpL rule + + +
- Canopy and ImpR rule + + +
- Canopy, contracted sequents and permutations + + +
+ - Definition of the uniform interpolant function via the Braga method + + +
- Basics + + +
- General preliminaries + + +
- Proof-theoretic preliminaries
+
-
+
- And and Or rules + + +
- Contracted sequents and permutations + + +
- Diamond equivalence
+
-
+
- N implies UI + + +
- Diamond N implies Diamond UI + + +
- Preliminaries of the remaining direction + + +
- Diamond UI implies Diamond N + + +
- Final equivalence + + +
+
+ - Correctness
+
-
+
- Variables + + +
- Entailment + + +
- Uniformity + + +
+
ISL.Environments
+-
+
- Overview: Environments + + +
- Connecting two kinds of multisets + + +
- A well-founded order and tactic on multi-sets + + +
- Multiset utilities + + +
- Conjunction, disjunction, and implication + + +
- A dependent version of `map` + + +
- Tactics + + +
ISL.Formulas
+-
+
- Overview: formulas + + +
- Definitions and notations. + + +
- Countability of the set of formulas + + +
- Weight + + +
ISL.Order
+ISL.PropQuantifiers
+-
+
- Overview: Propositional Quantifiers + + +
- Definition of propositional quantifiers. + + +
- Correctness
+
-
+
- (i) Variables + + +
- (ii) Entailment + + +
- Uniformity + + +
+ - Main uniform interpolation Theorem + + +
ISL.SequentProps
+-
+
- Overview: admissible rules in G4ip sequent calculus + + +
- Weakening + + +
- Inversion rules + + +
- Contraction + + +
- Admissibility of LJ's implication left rule + + +
- Correctness of optimizations + + +
- Generalized rules
+
-
+
- Generalized OrL and its invertibility + + +
- Generalized AndR + + +
- Generalized invertibility of AndR + + +
- Generalized AndL + + +
- Generalized OrR + + +
+
ISL.Sequents
+-
+
- Overview: Sequent calculus G4ip + + +
- Definition of provability in G4iSL + + +
- Tactics + + +