Automath ("matemáticas automatizadas") es un lenguaje formal , ideado por Nicolaas Govert de Bruijn a partir de 1967, para expresar teorías matemáticas completas de tal manera que un corrector de pruebas automatizado incluido pueda verificar su exactitud.
Descripción general
El sistema Automath incluyó muchas nociones novedosas que luego fueron adoptadas y / o reinventadas en áreas como el cálculo lambda mecanografiado y la sustitución explícita . Los tipos dependientes es un ejemplo destacado. Automath fue también el primer sistema práctico que aprovechó la correspondencia Curry-Howard . Las proposiciones se representaban como conjuntos (llamados "categorías") de sus pruebas, y la cuestión de la demostrabilidad se convirtió en una cuestión de no vacuidad (habitabilidad tipo ); de Bruijn desconocía el trabajo de Howard y declaró la correspondencia de forma independiente. [1]
LS van Benthem Jutting, como parte de este Ph.D. tesis en 1976, tradujo los Fundamentos del análisis de Edmund Landau a Automath y comprobó su corrección.
Sin embargo, Automath nunca se publicitó ampliamente en ese momento, por lo que nunca logró un uso generalizado; no obstante, resultó muy influyente en el desarrollo posterior de marcos lógicos y asistentes de prueba . [2] [3] El sistema Mizar , un sistema de escritura y verificación de las matemáticas formalizadas que todavía está en uso activo, fue influenciado por Automath.
Ver también
Referencias
- ^ Morten Heine Sørensen, Paweł Urzyczyn, Conferencias sobre el isomorfismo Curry-Howard , Elsevier, 2006, ISBN 0-444-52077-5 , págs. 98-99
- ^ RP Nederpelt, JH Geuvers, RC de Vrijer (1994) Artículos seleccionados sobre Automath. Vol. 133 de Studies Logic, Elsevier, Amsterdam. ISBN 0-444-89822-0 .
- ^ F. Kamareddine (2003) Treinta y cinco años de automatización de las matemáticas. Workshop, Dordrecht, Boston, publicado por Kluwer Academic Publishers, ISBN 1-4020-1656-5 .
enlaces externos
- El Archivo Automath (espejo)
- Treinta y cinco años de Automath página de inicio de un taller para celebrar los 35 años de Automath
- Página de Automath de Freek Wiedijk