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 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), (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), , 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), , 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]