A Closer Look at Some Recent Proof Compression-Related Claims

Michael C. Chavrimootoo, Ethan Ferland, Erin Gibson +1

Gordeev and Haeusler [GH19] claim that each tautology $\rho$ of minimal propositional logic can be proved with a natural deduction of size polynomial in $|\rho |$. This builds on work fro…