The problem of Pi_2-cut-introduction

TL;DR

This paper introduces an algorithmic method for proof compression by inserting Pi_2-cuts into cut-free LK-proofs, extending previous methods for Pi_1-cuts and achieving exponential compression.

Contribution

It presents a novel algorithm that constructs Pi_2-cut formulas and proofs, extending prior work on cut introduction and proof compression techniques.

Findings

Achieves exponential proof compression.

Extends methods from Pi_1-cuts to Pi_2-cuts.

Provides an algorithm for constructing Pi_2-cut formulas.

Abstract

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 cut-elimination method and extends former methods for introducing Pi_1-cuts. The Herbrand instances of a cut-free proof pi of a sequent S are described by a grammar G which encodes substitutions defined in the elimination of quantified cuts. We present an algorithm which, given a grammar G, constructs a Pi_2-cut formula A and a proof phi of S with one cut on A. It is shown that, by this algorithm, we can achieve an exponential proof compression.