Автомат
-
Обзор Automath
- Разработан Николасом Говертом де Брейном в 1967 году для автоматизации математических теорий.
- Включает новые понятия, которые позже были использованы в типизированном лямбда-исчислении и явной подстановке.
- Предложил концепцию зависимых типов и был первой практической системой с соответствием Карри-Говарда.
-
Применение и влияние
- Утверждения представлены в виде категорий доказательств, а доказуемость определяется как непустота.
- В 1976 году ван Бентем перевел «Основы анализа» Ландау на Automath и проверил его корректность.
- Несмотря на отсутствие широкой рекламы, оказал влияние на развитие логических структур и средств доказательства.
- Система Mizar, активно используемая для записи и проверки формализованной математики, была вдохновлена Automath.
-
Дополнительные ресурсы
- Ссылки на семинар, посвященный 35-летию Automath, и страницу Automath от Freek Wiedijk.
- Статья является заглушкой и призывает к расширению для улучшения Википедии.
Полный текст статьи: