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 metadatas

Cited literature [61 references]  Display  Hide  Download

https://hal-ecp.archives-ouvertes.fr/hal-00782857
Contributor : Marc Aiguier <>
Submitted on : Wednesday, January 30, 2013 - 4:58:18 PM
Last modification on : Friday, June 29, 2018 - 12:11:52 PM
Long-term archiving on : Monday, June 17, 2013 - 5:44:05 PM

File

Logica-Universalis10.pdf
Publisher files allowed on an open archive

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

303

Files downloads

314