Automath: Difference between revisions
Appearance
Content deleted Content added
Added disambiguation link for Autodidact |
No edit summary |
||
Line 1: | Line 1: | ||
{{otheruses4|the programming language|self-taught individuals| |
{{otheruses4|the programming language|self-taught individuals|Autodidacticism}} |
||
'''Automath''' (automating mathematics) is a [[programming language]], devised by [[Nicolaas Govert de Bruijn]], for expressing complete mathematical theories in such a way that a [[Theorem prover]] can verify the correctness. |
'''Automath''' (automating mathematics) is a [[programming language]], devised by [[Nicolaas Govert de Bruijn]], for expressing complete mathematical theories in such a way that a [[Theorem prover]] can verify the correctness. |
Revision as of 08:34, 28 November 2007
Automath (automating mathematics) is a programming language, devised by Nicolaas Govert de Bruijn, for expressing complete mathematical theories in such a way that a Theorem prover can verify the correctness.
References
Kamareddine, Fairouz (2003) Thirty-five years of automating mathematics. Dordrecht ; Boston : Kluwer Academic Publishers. ISBN 1402016565
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