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

Metadatas

Date

May 13, 2016

type
Language
Identifiers
License

info:eu-repo/semantics/OpenAccess


Keywords

Démonstration Gerhard Gentzen (1909-1945) Logique

Similar subjects Fr

Standardisation

Cite this document

Jules Chouquet, « L'identité des preuves : normalisation, réseaux et séparation », Dépôt Universitaire de Mémoires Après Soutenance, ID : 10670/1.u6kgep


Metrics


Share / Export

Abstract 0

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.

From the same authors

On the same subjects

Similar documents