Автомат

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

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

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

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

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

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

Это манифест

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

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

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

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

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

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

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

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

[1]

[2]

[3]