“cut”的概念、定义、翻译、参考文献-科学参考

cut

Statistics

See network flow problem.

Chemical Engineering

A division in separating distilled products of differing compositions or purities from a distillation process based on composition or temperature. In the continuous fractionation of crude oil, the naphtha cut, which contains a number of different hydrocarbon compounds, has a boiling point range of around 35°C to 200°C. In the batch distillation of whisky, the differential compositions of alcohol are termed the foreshots and feints whose composition is determined by specific gravity.

Computer

1. To mark a piece of text or graphical information in some way, read it into a temporary storage location, and delete it from the original document. The information may then be inserted into a new location. This has the effect of moving the information from one location to another and is often called a move, or cut and paste by analogy with scissors and glue techniques. See clipboard. Compare copy.
2. A mechanism used in Prolog to limit backtracking. Roughly speaking, the effect of a cut is to fix certain decisions that have already been made, thus preventing the system from undoing those decisions in order to perform a further search for solutions to its goals. This is a way of avoiding costly search known in advance to be fruitless, or of excluding alternative solutions that are not wanted. However, writing cuts in a program makes its behaviour dependent on the system’s search sequence. Such dependency prevents the program from being a pure statement of logical relationships and thus goes against the spirit of logic programming.

Logic

In proof theory, the structural inference rule
$\frac{Γ \Rightarrow Δ, φ Γ^{'}, φ \Rightarrow Δ^{'}}{Γ, Γ^{'} \Rightarrow Δ, Δ^{'}} Cut$
Cut differs from other rules encountered in sequent calculi in an important way. In the other rules, e.g., a sequent calculus for classical logic, inferences preserve subformulae from upper to lower sequent. For example, in applications of an elimination rule, every subformula in the auxiliary formula appears in the principal formulae. In the above representation of cut, however, the formula $φ$ (the ‘cut formula’) and its subformulae are completely absent in the lower sequent (unless they appear in some side formula).
Hence, it has historically been an important task to prove that a sequent calculus allows cut elimination, that is, that when cut is not taken as a primitive inference, cut is still an admissible inference. When a sequent calculus has cut elimination, any proof that employs the cut rule can be emulated by a proof in which cut is not employed, that is, if a sequent is provable, then it has a cut-free proof. Logician Gerhard Gentzen (1909–1945) proved cut elimination for his sequent calculi for classical and intuitionistic logics in the famous Hauptsatz or cut elimination theorem.

单词	cut
释义	cut Statistics See network flow problem. Chemical Engineering A division in separating distilled products of differing compositions or purities from a distillation process based on composition or temperature. In the continuous fractionation of crude oil, the naphtha cut, which contains a number of different hydrocarbon compounds, has a boiling point range of around 35°C to 200°C. In the batch distillation of whisky, the differential compositions of alcohol are termed the foreshots and feints whose composition is determined by specific gravity. Computer 1. To mark a piece of text or graphical information in some way, read it into a temporary storage location, and delete it from the original document. The information may then be inserted into a new location. This has the effect of moving the information from one location to another and is often called a move, or cut and paste by analogy with scissors and glue techniques. See clipboard. Compare copy. 2. A mechanism used in Prolog to limit backtracking. Roughly speaking, the effect of a cut is to fix certain decisions that have already been made, thus preventing the system from undoing those decisions in order to perform a further search for solutions to its goals. This is a way of avoiding costly search known in advance to be fruitless, or of excluding alternative solutions that are not wanted. However, writing cuts in a program makes its behaviour dependent on the system’s search sequence. Such dependency prevents the program from being a pure statement of logical relationships and thus goes against the spirit of logic programming. Logic In proof theory, the structural inference rule $\frac{Γ \Rightarrow Δ, φ Γ^{'}, φ \Rightarrow Δ^{'}}{Γ, Γ^{'} \Rightarrow Δ, Δ^{'}} Cut$ Cut differs from other rules encountered in sequent calculi in an important way. In the other rules, e.g., a sequent calculus for classical logic, inferences preserve subformulae from upper to lower sequent. For example, in applications of an elimination rule, every subformula in the auxiliary formula appears in the principal formulae. In the above representation of cut, however, the formula $φ$ (the ‘cut formula’) and its subformulae are completely absent in the lower sequent (unless they appear in some side formula). Hence, it has historically been an important task to prove that a sequent calculus allows cut elimination, that is, that when cut is not taken as a primitive inference, cut is still an admissible inference. When a sequent calculus has cut elimination, any proof that employs the cut rule can be emulated by a proof in which cut is not employed, that is, if a sequent is provable, then it has a cut-free proof. Logician Gerhard Gentzen (1909–1945) proved cut elimination for his sequent calculi for classical and intuitionistic logics in the famous Hauptsatz or cut elimination theorem.
随便看	ITU-R Iturbide, Agustín de (1783–1824) ITU-T i-type semiconductor IU IUE IUGS IUPAC IUPAP IUS IVA Ivan III (1440–1505) Ivan IV (1530–84) Ivanovsky, Dmitri Iosifovich IVD Ivins, Marsha Sue (1951– ) Ivorian Ivory Coast IVR ivy I-wave I-way IX stoss stoss and lee