Automath theorem prover
From Wikipedia, the free encyclopedia
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
- ^ R. P. Nederpelt, J. H.Geuvers, R. C. de Vrijer (1994) Selected Papers on Automath. Vol. 133 of Studies Logic, Elsevier, Amsterdam. ISBN 0 444 89822 0.
- ^ F. Kamareddine (2003) Thirty-five years of automating mathematics. Workshop, Dordrecht, Boston, published by Kluwer Academic Publishers, ISBN 1402016565.
[edit] External links
- Automath Archive - in honour of prof. N.G. de Bruijn
- The Automath Archive (mirror)
- Thirty Five years of Automath homepage of a workshop to celebrate the 35th year of Automath
- Automath page by Freek Wiedijk
 |
This logic-related article is a stub. You can help by expanding it. |
