Some General Results About Proof Normalization

摘要

In this paper, we provide a general setting under which resultsof normalization of proof trees such as, for instance, the logicality result inequational reasoning and the cut-elimination property in sequent or nat-ural deduction calculi, can be unified and generalized. This is achieved bygiving simple conditions which are sufficient to ensure that such normal-ization results hold, and which can be automatically checked since theyare syntactical. These conditions are based on basic properties of elemen-tary combinations of inference rules which ensure that the induced globalproof tree transformation processes do terminate.