From the text: The first cut-elimination procedure for infinitary calculi was published by P. S. Novikov in 1943. As distinct from the well-known cut-elimination procedure by G. Gentzen for the (finite) predicate calculus, Novikov’s procedure in its essential part is a procedure of converting regular (cutfree in modern terminology) derivations into regular derivations of some conjunctive and disjunctive forms of the derived formula.
During the 1950’s several individuals generalized Gentzen’s procedure to infinitary calculi. The scheme of such generalizations is the following:
1) for some (perhaps all) cuts in a derivation a certain reduction step is defined; this step (in the first approximation) may be thought of as a transposition of the reducing cut with one of its adjoining rules;
2) a reduction strategy (a strategy of choice of a cut and adjoining rule for reduction) leading each derivation to a cutfree derivation of the same formula is pointed out.
Note that different reduction strategies applied to the same derivation may lead to different cutfree forms.
The main result of the present paper is a construction of such a strategy of Gentzen-type reductions, which, when applied to derivations allowing Novikov’s procedure, give the same cutfree form.
For the entire collection see [Zbl 0954.00500].