Algorithmic introduction of quantified cuts

We describe a method for inverting Gentzen's cut-elimination in classical first-order logic. Our algorithm is based on first computing 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. Concerning asymptotic complexity, this method allows an exponential compression of quantifier complexity (the number of quantifier-inferences) of proofs.