Schnittregel
# Schnittregel

Der Schnitt (engl. cut oder cut-rule) ist eine transitive Regel in der Logik, der linearen Optimierung und der Constraintprogrammierung.

Die Aussage der Schnittregel lässt sich im Wesentlichen so zusammenfassen: Wird in einer Ableitung oder einem Suchbaum ein vermeidbarer transitiver „Umweg“ vorgenommen, so ist dieser Umweg wegschneidbar.

## Schnitt in der Logik

In den Logikkalkülen ist die Schnittregel der modus ponens auf metalogischer Stufe und lautet so:

* $\qquad {\frac {\Gamma \vdash A\qquad A,\Delta \vdash B}{\Gamma ,\Delta \vdash B}}$

Dass die Schnittregel in den Gentzentyp-Kalkülen zulässig (eliminierbar) ist, besagt der Gentzensche Hauptsatz.

