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.
Type de document :
Article dans une revue
Logica Universalis, Springer Verlag, 2010, 4 (1), pp.1-29. 〈10.1007/s11787-010-0011-4〉
Liste complète des métadonnées

Littérature citée [61 références]  Voir  Masquer  Télécharger

https://hal-ecp.archives-ouvertes.fr/hal-00782857
Contributeur : Marc Aiguier <>
Soumis le : mercredi 30 janvier 2013 - 16:58:18
Dernière modification le : vendredi 29 juin 2018 - 12:11:52
Document(s) archivé(s) le : lundi 17 juin 2013 - 17:44:05

Fichier

Logica-Universalis10.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

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〉

Partager

Métriques

Consultations de la notice

228

Téléchargements de fichiers

180