Automath (pour ) é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 ) 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. 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.
Références
Liens internes correspondance de Curry-Howard lambda-calcul assistant de preuve 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
Catégorie:Assistant de preuve Catégorie:Théorie des types