Schnittregel

aus Wikipedia, der freien Enzyklopädie
Zur Navigation springen Zur Suche springen

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

[Bearbeiten | Quelltext bearbeiten]

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

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