Abstract

In this paper we first give a survey of reductive cut-elimination methods in classical logic. In particular we describe the methods of Gentzen and Schütte-Tait from the abstract point of view of proof reduction. We also present the method CERES which we classify as a semi-semantic method. In a further section we describe the so-called semantic methods. In the second part of the paper we carry the proof analysis further by generalizing the CERES method to CERESD . In the generalized version CERESD we admit general elimination rules which are based on the mere semantical truth of sentences. We construct complete cut-free LK-derivations originating from derivations potentially containing unproven lemmas. Finally we give a comparison of reductive methods and CERESD by presenting a general simulation result.