Автомат

Automath («автоматизирующая математика») - это формальный язык , разработанный Николаасом Говертом де Брюйном, начиная с 1967 года, для выражения полных математических теорий таким образом, чтобы включенная автоматическая программа проверки доказательств могла проверить их правильность.

Обзор [ править ]

Система Automath включала множество новых понятий, которые позже были приняты и / или заново изобретены в таких областях, как типизированное лямбда-исчисление и явная подстановка . Зависимые типы - один из ярких примеров. Automath был также первой практической системой, которая использовала соответствие Карри – Ховарда . Предложения были представлены в виде наборов (называемых «категориями») их доказательств, и вопрос доказуемости превратился в вопрос непустоты ( тип обитания ); де Брёйн не знал о работе Говарда и независимо изложил переписку. ^[1]

LS van Benthem Jutting, как часть этого доктора философии. В своей диссертации в 1976 году « Основы анализа» Эдмунда Ландау были переведены на автомат и проверили их правильность.

Однако в то время Automath не получил широкой огласки и поэтому не получил широкого распространения; тем не менее, он оказался очень влиятельным в более позднем развитии логических структур и помощников доказательства . ^[2]^[3] Система Mizar , система записи и проверки формализованной математики, которая все еще активно используется, находилась под влиянием Automath.

См. Также [ править ]

Манифест QED

Ссылки [ править ]

^ Мортен Гейне Соренсен, Павел Уржичин, Лекции по изоморфизму Карри-Ховарда , Elsevier, 2006, ISBN 0-444-52077-5 , стр 98-99
^ RP Nederpelt, JH Geuvers, RC de Vrijer (1994) Избранные статьи по автоматизации. Vol. 133 исследований логики, Elsevier, Амстердам. ISBN 0-444-89822-0 .
^ Ф. Камареддин (2003) Тридцать пять лет автоматизации математики. Workshop, Dordrecht, Boston, опубликовано Kluwer Academic Publishers, ISBN 1-4020-1656-5 .

Внешние ссылки [ править ]

Архив автоматов (зеркало)
Тридцать пять лет Automath - домашняя страница семинара, посвященного 35-летию Automath
Страница автомата, автор Freek Wiedijk

Эта статья, посвященная формальным методам, является незавершенной . Вы можете помочь Википедии, расширив ее .

[1] Мортен Гейне Соренсен, Павел Уржичин, Лекции по изоморфизму Карри-Ховарда , Elsevier, 2006, ISBN 0-444-52077-5 , стр 98-99

[2] RP Nederpelt, JH Geuvers, RC de Vrijer (1994) Избранные статьи по автоматизации. Vol. 133 исследований логики, Elsevier, Амстердам. ISBN 0-444-89822-0 .

[3] Ф. Камареддин (2003) Тридцать пять лет автоматизации математики. Workshop, Dordrecht, Boston, опубликовано Kluwer Academic Publishers, ISBN 1-4020-1656-5 .

[1]