Schnittregel
aus Wikipedia, der freien Enzyklopädie
Der Schnitt (engl. cut oder cut-rule) ist eine transitive Regel in der Logik, der linearen Optimierung und der Constraintprogrammierung.
Wird in einer Ableitung oder einem Suchbaum ein unnötiger transitiver Umweg vorgenommen, so ist dieser Umweg wegschneidbar.
[Bearbeiten] Schnitt in der Logik
In den Logikkalkülen ist die Schnittregel der modus ponens auf metalogischer Stufe und lautet so:
Ist A aus Sequenzen herleitbar und mittels A auch B herleitbar, so ist B herleitbar. A wird also weggeschnitten.
Dass die Schnittregel in den Gentzentyp-Kalkülen zulässig und eliminierbar ist, besagt der Gentzensche Hauptsatz.
[Bearbeiten] Schnitt in der Optimierung, Programmierung, Topologischen Sortierung
Im Branch-and-Bound-Verfahren ist das Bounding (Begrenzen) ein Wegschneiden (auch: cutting-plane Methode) von Zweigen eines Optimierungsbaums. Eine Optimierung des Minimax-Algorithmus' bei Spielen ist der Alpha-Beta-Cut.
Die so genannte Constraintprogrammierung ist den Regelkalkülen verwandt. Hier versucht man schnittfrei (engl. cut-free) zu programmieren. Durch schnittfreie Suchbäume wird die Beweissuche (proof search) vereinfacht. Es entstehen Topologisch sortierbare Graphen.
Es gibt so genannte grüne Schnitte, die Zweige des Suchbaums wegschneiden, die keine Lösung enthalten. Rote Schnitte schneiden Zweige weg, die Lösungen enthalten.
[Bearbeiten] 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
- Dakin, R. J. (1965). A tree-search algorithm for mixed integer programming problems.
In: The Computer Journal, Volume 8, S. 250-255 - Land, A. H. und A. G. Doig (1960). An automatic method of solving discrete programming problems.
In: Econometrica 28, S. 497-520 - Irvin J. Lustig, Jean-Fr. PugetConstraint and Mathematical Programming
