A master 1 project implementing Hudelmaier's algorithm for deciding the provability of a sequent in intuitionistic propositional logic.
.
├── README.md
├── _CoqProject
├── theories
│ ├── base.v
│ ├── listSplitting.v
│ ├── misc.v
│ ├── strongInduction.v
│ ├── introRules.v
│ ├── elimRules.v
│ ├── decider.v (contains is_provable_rec)
│ ├── examples.v
- Quentin Schroeder (M1 MPRI Paris Cite, 2023-2024)