Cutting rule
The interface (English, cut or cut-rule) is a transitive rule of logic, linear programming and constraint programming .
If an avoidable transitive “detour” is made in a derivation or a search tree , this detour can be cut away.
Cut in logic
In the logic calculi the rule of intersection is the modus ponens on a metalogical level and reads as follows:
Gentzen's law states that the rule of intersection in the Gentzen-type calculus is permissible (eliminable) .
literature
- Gerhard Gentzen: Investigations into logical reasoning. Mathematical Journal 39 (1934). Reprinted in: Karel Berka , Lothar Kreier: Logic Texts , Berlin (East) 1986
- Jean-Yves Girard: Proofs and Types Cambridge University Press 1989; reprint web 2003 (PDF file; 925 kB)