Herbrand's theorem states that an existential formula is provable in classical first-order logic iff a finite disjunction of instances is a propositional tautology. This theorem and appropriate extensions of it can be used for representing proofs with and without cuts in a compact way.

I will speak about this representation and its algorithmic advantages in certain classes of proofs: 1) it allows cut-elimination procedures without syntactic bureaucracy and 2) it makes it possible to algorithmically reverse cut-elimination: by finding sufficiently similar parts of a cut-free proof and identifying them by introduction of a cut the proof is abbreviated.