Jump to content

Automath

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by Ironwolf (talk | contribs) at 08:34, 28 November 2007. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

This article is about the programming language. For self-taught individuals, see 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.

References

Kamareddine, Fairouz (2003) Thirty-five years of automating mathematics. Dordrecht ; Boston : Kluwer Academic Publishers. ISBN 1402016565

Stub icon

This logic-related article is a stub. You can help Wikipedia by expanding it.

Comp Sci logo This computer science-related article is a stub. You can help Wikipedia by expanding it.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Automath&oldid=174328465"