Schnittelimination (Cut-Elimination)

Ein Verfahren in der Beweistheorie, das einen Sequenz- (oder natürliche Deduktions-)Beweis so umformt, dass Cut‑Schlüsse (Anwendungen der ‚cut‘‑Regel) entfernt werden und ein cut‑freier Beweis mit der Unterformel‑Eigenschaft entsteht.

Die Beweistransformation, die Cut-Inferenzen (Anwendungen der Cut-Regel) aus einem sequentenkalkülartigen Beweis entfernt, um eine cutfreie Herleitung desselben Endsequents zu erzeugen, wobei die Beweisbarkeit erhalten bleibt, die Struktur und Größe des Beweises sich jedoch oft ändern.