In the recent past, the reduction-based and the model-based methods to prove cut elimination have converged, so that they now appear just as two sides of the same coin. This paper details some of the steps of this transformation.

翻译：近年来，基于归约与基于模型的割消证明方法已趋于收敛，二者如今犹如一枚硬币的两面。本文详细阐述了这一转变过程中的若干关键步骤。