|
This article is about the programming language. For self-taught individuals, see Autodidacticism.
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 the correctness. The Automath system included many notions that were later adopted and/or reinvented in areas such as typed lambda calculus and explicit substitution. Automath was never widely publicized at the time, however, and so never achieved widespread use, and is now mostly of historic interest.[1][2] [edit] References
[edit] External links
Directorio de Enlaces Directorio dmoz Directorio espejo dmoz Pedro Bernardo |