Algorithmic Introduction of Quantified Cuts

TL;DR

This paper introduces a method to invert cut-elimination in classical first-order logic, enabling exponential proof compression by computing compressed representations and constructing corresponding cut-formulas, with practical implementation details.

Contribution

It presents a novel algorithm for inverting cut-elimination that achieves exponential proof compression and can be applied to automated theorem prover outputs.

Findings

Achieves exponential proof size reduction

Applicable to automated theorem prover outputs

Provides an implementable algorithm

Abstract

We describe a method for inverting Gentzen's cut-elimination in classical first-order logic. Our algorithm is based on first computign a compressed representation of the terms present in the cut-free proof and then cut-formulas that realize such a compression. Finally, a proof using these cut-formulas is constructed. This method allows an exponential compression of proof length. It can be applied to the output of automated theorem provers, which typically produce analytic proofs. An implementation is available on the web and described in this paper.