Automath

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

Automath (pour « automating mathematics ») était un langage formel, développé par Nicolaas Govert de Bruijn à partir de 1967, dont le but était d'exprimer des théories mathématiques complètes de manière à inclure un assistant de preuve qui pouvait en vérifier la correction.

Le système Automath apportait de nombreuses notions novatrices qui ont été adoptées ou réinventées ultérieurement, comme le lambda-calcul typé et la substitution explicite. La notion de type dépendant en est un exemple paradigmatique. Automath était aussi le premier système pratique qui exploitait la correspondance de Curry-Howard. Les propositions étaient représentées comme les ensembles (appelées « catégories ») de leurs preuves, et la problème de leur preuve se ramenait à tester le vide d'ensembles ; de Bruijn ne connaissait pas les travaux de Howard, et a énoncé la correspondance indépendamment[1]. Automath n'a pas été largement publié à l'époque, et n'a pas été utilisé à large échelle ; mais c'est un système précurseur des assistants de preuve actuels[2],[3].

Références[modifier | modifier le code]

  1. (en) Morten Heine Sørensen et Paweł Urzyczyn, Lectures on the Curry-Howard Isomorphism, North-Holland Publishing Co., coll. « Studies in Logic and the Foundations of Mathematics » (no 149),‎ 2006 (ISBN 0-444-52077-5), p. 98-99.
  2. (en) Rob P. Nederpelt, J. H. Geuvers et Roel C. de Vrijer (éditeurs), Selected papers on Automath, North-Holland Publishing Co., coll. « Studies in Logic and the Foundations of Mathematics » (no 133),‎ 1994, xx+1024 p. (ISBN 0-444-89822-0).
  3. (en) Fairouz D. Kamareddine (éditeur), Thirty-five years of automating mathematics : Dedicated to 35 years of de Bruijn's Automath, Dordrecht, Kluwer Academic Publishers, coll. « Applied Logic Series » (no 28),‎ 2003, x+318 p. (ISBN 1-4020-1656-5).

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Automath » (voir la liste des auteurs)

Liens internes[modifier | modifier le code]

Liens externes[modifier | modifier le code]