Portail:Logique/Le saviez-vous?/Avril

Une page de Wikipédia, l'encyclopédie libre.

La logique linéaire inventée par le logicien Jean-Yves Girard en 1986, est un produit de la théorie de la démonstration moderne. Elle résulte d'une analyse du comportement des preuves des logiques classique et intuitionniste au travers de la procédure d'élimination des coupures introduite par Gentzen en 1936 pour prouver son Hauptsatz (un résultat fondamental en logique).