Article ID Journal Published Year Pages File Type
6875742 Theoretical Computer Science 2018 34 Pages PDF
Abstract
We describe an algorithmic method of proof compression based on the introduction of Π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 Π1-cuts. The Herbrand instances of a cut-free proof π 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 Π2-cut formula A and a proof π′ of S with one cut on A. It is shown that, by this algorithm, we can achieve an exponential proof compression.
Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, ,