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:
{\displaystyle \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.
Literatur
[Bearbeiten | Quelltext bearbeiten ]- Gerhard Gentzen: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39 (1934). Nachdruck in: Karel Berka, Lothar Kreier: Logik-Texte, Berlin (Ost) 1986
- Jean-Yves Girard: Proofs and Types Cambridge University Press 1989; reprint web 2003 (PDF-Datei; 925 kB)