Cut Elimination

A procedure in proof theory that transforms a sequent (or natural deduction) proof to remove cut inferences (applications of the 'cut' rule), producing a cut-free proof typically satisfying the subformula property.

The proof transformation that removes cut inferences (applications of the cut rule) from a sequent-calculus style proof to produce a cut-free derivation of the same end-sequent, preserving provability while often changing proof structure and size.