The problem of Pi_2-cut-introduction

Alexander Leitsch, Michael Peter Lettmann

We describe an algorithmic method of proof compression based on the introduction of Pi_2-cuts into a cut-free LK-proof. The current approach is based on an inversion of Gentzen s c…