The author discusses a simplified form of Gentzen’s sequential calculus as a basis for discussing proof procedures. He shows that the cut rule used in Gentzen’s approach, although redundant, can lead to much shorter proofs, or rather that eliminating the use of the cut rule from a proof results in an exponentially longer initial sequence.

He then goes on to point out that in resolution proofs, the cut rule appears in more than one guise. This can dramatically reduce the length of some proofs compared to the cut-free analysis trees in the Gentzen calculus. This reduction is not universal, however, especially if one applies refinement techniques (such as input resolution and linear resolution) to the general resolution method.

Zhang uses these results to discuss the efficiencies of mechanical proofs (using resolution or Bibel’s connection calculus) and those special proofs that are used by Prolog.