Automath

Automath ("automating mathematics") is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness.

Overview

The Automath system included many novel notions that were later adopted and/or reinvented in areas such as typed lambda calculus and explicit substitution. Dependent types is one outstanding example. Automath was also the first practical system that exploited the Curry–Howard correspondence. Propositions were represented as sets (called "categories") of their proofs, and the question of provability became a question of non-emptiness (type inhabitation); de Bruijn was unaware of Howard's work, and stated the correspondence independently.^[1]

L. S. van Benthem Jutting, as part of this Ph.D. thesis in 1976, translated Edmund Landau's Foundations of Analysis into Automath and checked its correctness.

Automath was never widely publicized at the time, however, and so never achieved widespread use; nonetheless, it proved very influential in the later development of logical frameworks and proof assistants.^[2]^[3] The Mizar system, a system of writing and checking formalized mathematics that is still in active use, was influenced by 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]