Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6875742 | Theoretical Computer Science | 2018 | 34 Pages |
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
Alexander Leitsch, Michael Lettmann,