A simple proof that super consistency implies cut elimination

Abstract : We give a simple proof of the cut elimination theorem for super-consistent theories in natural deduction modulo, inspired by proof normalization, but without explicit proofs. It can also be formulated as a completeness proof for the cut free calculus. This formulation involves some kind of V-complexes. We then discuss application to simple types theory and the links, in this case, with the normalization and purely semantical methods, in particular those using V-complexes.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal-mines-paristech.archives-ouvertes.fr/hal-00743256
Contributeur : Claire Medrala <>
Soumis le : jeudi 18 octobre 2012 - 15:25:07
Dernière modification le : jeudi 4 avril 2019 - 01:31:12
Document(s) archivé(s) le : samedi 19 janvier 2013 - 03:39:38

Fichiers

Identifiants

Collections

Citation

Gilles Dowek, Olivier Hermant. A simple proof that super consistency implies cut elimination. 18th International Conference, RTA 2007, Jun 2007, Paris, France. pp.Pages 93-106, ⟨10.1007/978-3-540-73449-9_9⟩. ⟨hal-00743256⟩

Partager

Métriques

Consultations de la notice

229

Téléchargements de fichiers

255