L'identité des preuves : normalisation, réseaux et séparation

Résumé : La théorie de la démonstration présente divers systèmes formels de preuve permettant de représenter des démonstrations à l’aide d’objets rigoureusement définis, et dont la manipulation revêt divers intérêts. Nous nous proposons ici d’étudier la question — très débattue — de savoir à quelles conditions deux dérivations de ces systèmes représentent, décrivent, la même démonstration. Nous étudions en particulier deux propositions de réponses, avant de mettre chacune en perspective pour une meilleure compréhension des concepts et appareils sollicités. Ces deux solutions correspondent respectivement à une relation d’équivalence induite par le processus de normalisation des dérivations défini par Gentzen dans les années 1930, et à un quotient par une représentation graphique des dérivations due à Girard (dans les années 1980) que sont les réseaux de preuve.
Type de document :
Mémoires
Philosophie. 2016
Liste complète des métadonnées

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

https://dumas.ccsd.cnrs.fr/dumas-01427107
Contributeur : Paris 1 Panthéon-Sorbonne - Ufr Philosophie <>
Soumis le : mercredi 22 février 2017 - 09:30:24
Dernière modification le : vendredi 29 septembre 2017 - 20:35:04
Document(s) archivé(s) le : mardi 23 mai 2017 - 13:20:01

Identifiants

  • HAL Id : dumas-01427107, version 1

Citation

Jules Chouquet. L'identité des preuves : normalisation, réseaux et séparation. Philosophie. 2016. 〈dumas-01427107〉

Partager

Métriques

Consultations de la notice

190

Téléchargements de fichiers

197