imported>SchlurcherBot: Bot: http → https

2025-12-27T14:21:05Z

Bot: http → https

Neue Seite

Der '''Schnitt''' (engl. '''cut''' oder cut-rule) ist eine [[Transitive Relation|transitive]] Regel in der Logik, der [[lineare Optimierung|linearen Optimierung]] und der [[Constraintprogrammierung]].

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

== Schnitt in der Logik ==
In den [[Kalkül|Logikkalkül]]en ist die Schnittregel der [[modus ponens]] auf metalogischer Stufe und lautet so:
{|style="margin-left:2em"
|<math>\qquad\frac{\Gamma\vdash A\qquad A, \Delta\vdash B}{\Gamma, \Delta\vdash B}</math>
|}
Dass die Schnittregel in den [[Sequenzenkalkül|Gentzentyp-Kalkülen]] [[Zulässige Regel|zulässig]] (eliminierbar) ist, besagt der [[Gentzenscher Hauptsatz|Gentzensche Hauptsatz]].

== Literatur ==
*Gerhard Gentzen: Untersuchungen über das logische Schließen. [https://www-gdz.sub.uni-goettingen.de/cgi-bin/digbib.cgi?PPN266833020_0039 ''Mathematische Zeitschrift'' 39] (1934). Nachdruck in: [[Karel Berka]], Lothar Kreier: ''Logik-Texte'', Berlin (Ost) 1986
*Jean-Yves Girard: [http://www.cs.man.ac.uk/~pt/stable/prot.pdf Proofs and Types Cambridge University Press 1989; reprint web 2003] (PDF-Datei; 925 kB)

[[Kategorie:Mathematische Logik]]
[[Kategorie:Theoretische Informatik]]

[[en:cut-elimination]]

Schnittregel - Versionsgeschichte

imported>SchlurcherBot: Bot: http → https