Skip to Main content Skip to Navigation
Journal articles

Some General Results About Proof Normalization

Abstract : In this paper, we provide a general setting under which results of normalization of proof trees such as, for instance, the logicality result in equational reasoning and the cut-elimination property in sequent or natural deduction calculi, can be unified and generalized. This is achieved by giving simple conditions which are sufficient to ensure that such normalization results hold, and which can be automatically checked since they are syntactical. These conditions are based on basic properties of elementary combinations of inference rules which ensure that the induced global proof tree transformation processes do terminate.
Document type :
Journal articles
Complete list of metadata

Cited literature [61 references]  Display  Hide  Download
Contributor : Marc Aiguier Connect in order to contact the contributor
Submitted on : Wednesday, January 30, 2013 - 4:58:18 PM
Last modification on : Tuesday, July 20, 2021 - 3:05:15 AM
Long-term archiving on: : Monday, June 17, 2013 - 5:44:05 PM


Publisher files allowed on an open archive




Marc Aiguier, Longuet Delphine. Some General Results About Proof Normalization. Logica Universalis, Springer Verlag, 2010, 4 (1), pp.1-29. ⟨10.1007/s11787-010-0011-4⟩. ⟨hal-00782857⟩



Les métriques sont temporairement indisponibles