„Schnittregel“ – Versionsunterschied
| [ungesichtete Version] | [ungesichtete Version] |
Die Seite wurde neu angelegt: „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 Lo…“ |
K Textersetzung - „Kategorie:Mathematische Logik“ durch „Kategorie:mathematische Logik“ Markierung: Zurückgesetzt |
||
| Zeile 15: | Zeile 15: | ||
[[Kategorie: | [[Kategorie:mathematische Logik]] | ||
[[Kategorie:Theoretische Informatik]] | [[Kategorie:Theoretische Informatik]] | ||
[[en:cut-elimination]] | [[en:cut-elimination]] | ||
Version vom 17. September 2025, 18:53 Uhr
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:
Dass die Schnittregel in den Gentzentyp-Kalkülen zulässig (eliminierbar) ist, besagt der Gentzensche Hauptsatz.
Literatur
- 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)