Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

A simple proof that super consistency implies cut elimination

Abstract : We give a simple and direct proof that super-consistency implies the cut elimination property in deduction modulo. This proof can be seen as a simpli cation of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut-free calculus. As an application, we compare our work with the cut elimination theorems in higher-order logic that involve V-complexes.
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-00793008
Contributeur : Claire Medrala <>
Soumis le : jeudi 21 février 2013 - 14:29:24
Dernière modification le : jeudi 24 septembre 2020 - 16:36:01
Archivage à long terme le : : dimanche 2 avril 2017 - 03:34:13

Fichier

A-516.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Citation

Gilles Dowek, Olivier Hermant. A simple proof that super consistency implies cut elimination. Notre Dame Journal of Formal Logic, University of Notre Dame, 2012, 53 (4), pp. 93-106. ⟨10.1215/00294527-1722692⟩. ⟨hal-00793008⟩

Partager

Métriques

Consultations de la notice

558

Téléchargements de fichiers

317