# Algorithmic Introduction of Quantified Cuts

arXiv: https://arxiv.org/abs/1401.4330 · HTML: https://mlsanity.com/paper/1401.4330/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Jan 2014.

## Built on by (most cited first, 1 of 1)

- [Learning from Lukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)](https://mlsanity.com/paper/2104.13645/) (2021)

## Abstract (arXiv)

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.