Un article de Wikipedia.y-project.com.
La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve, a été fondée par David Hilbert au début du XXème siècle. Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au 2ème Congrès international de mathématiques en 1900 avec pour objectif de résoudre le problème de la cohérence des mathématiques. Cet objectif a été invalidé par le non moins célèbre théorème d'incomplétude de Kurt Gödel en 1931, ce qui n'a toutefois pas empêché la théorie de la démonstration de se développer, notamment grâce aux travaux de Jacques Herbrand et de Gerhard Gentzen. Ce dernier a démontré l'un des résultats principaux de la théorie de la démonstration, connu sous le nom de Hauptzatz (théorème principal) ou théorème d'élimination des coupures. Gentzen a ensuite utilisé ce théorème pour donner la première preuve purement syntaxique de la cohérence de l'arithmétique.
Après une période de calme, qui a tout de même permis d'établir un certain nombre d'autres résultats de cohérence relative et d'esquisser une classification des théories axiomatiques, la théorie de la démonstration a connu une renaissance spectaculaire au cours des années 60 avec la découverte de l'isomorphisme de Curry-Howard qui a exhibé un lien structurel nouveau et profond entre logique et informatique : essentiellement la procédure d'élimination des coupures définie par Gentzen peut être vue comme un processus de calcul, si bien que les démonstrations formelles deviennent alors des programmes. Depuis la théorie de la démonstration s'est développée en étroite symbiose avec d'autres domaines de la logique et de l'informatique théorique, notamment le lambda-calcul, et a donné naissance à de nouveaux modèles du calcul, le plus récent étant la logique linéaire de Jean-Yves Girard en 1986. Aujourd'hui une partie de la théorie de la démonstration se confond avec la sémantique des langages de programmation et interagit avec de nombreuses autres disciplines de la logique ou de l'informatique théorique :
Le Texte ci-dessus est disponible sous GNU Free Documentation License.
La source est wikipedia http://fr.wikipedia.org/wiki/Théorie de la démonstration
