Autómata

Automath ("automatización de las matemáticas") 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 verificador de pruebas automatizado incluido pueda comprobar su corrección.

El sistema Automath incluía muchas nociones novedosas que posteriormente fueron adoptadas o reinventadas en áreas como el cálculo lambda tipado y la sustitución explícita . Los tipos dependientes son un ejemplo destacado. Automath fue también el primer sistema práctico que aprovechó la correspondencia de 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 ( habitación de tipos ); de Bruijn desconocía el trabajo de Howard y enunció la correspondencia de forma independiente. ^{[ 1 ]}

L.S. van Benthem Jutting, como parte de su tesis doctoral en 1976, tradujo los Fundamentos del Análisis de Edmund Landau al idioma Automath y comprobó su corrección.

Sin embargo, Automath nunca fue ampliamente publicitado en su momento, por lo que nunca alcanzó un uso generalizado; no obstante, resultó muy influyente en el desarrollo posterior de marcos lógicos y asistentes de demostración . ^{[ 2 ] [ 3 ]} El sistema Mizar , un sistema para escribir y verificar matemáticas formalizadas que todavía se utiliza activamente, fue influenciado por Automath.

• Manifiesto QED

• El archivo de autómatas (espejo)
• Treinta y cinco años de Automath: página principal de un taller para celebrar el 35 aniversario de Automath.
• Página de automatización de Freek Wiedijk