Automath
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 la substitution explicite ou la notion de type dépendant dont Automath 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 le problème de l'existence de preuve se ramenait à tester la vacuité d'un ensemble ; 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é à grande échelle ; mais c'est un système précurseur des assistants de preuve actuels[2] - [3].
Références
- (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), , 442 p. (ISBN 978-0-444-52077-7), p. 98-99.
- (en) Rob P. Nederpelt, J. H. Geuvers et Roel C. de Vrijer (éditeurs), Selected papers on Automath, Amsterdam/Lausanne/New York etc., North-Holland Publishing Co., coll. « Studies in Logic and the Foundations of Mathematics » (no 133), , xx+1024 (ISBN 978-0-444-89822-7).
- (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 (ISBN 978-1-4020-1656-1, présentation en ligne).
Liens internes
Liens externes
- The Automath Archive (miroir)
- Thirty Five years of Automath Site d'un colloque célébrant les 35 ans d'Automath
- Page Automath par Freek Wiedijk