Automath: Difference between revisions

Content deleted Content added

Inline

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.

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

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

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

Revision as of 08:33, 28 November 2007 edit Ironwolf (talk \| contribs) 304 edits Added disambiguation link for Autodidact ← Previous edit		Revision as of 08:34, 28 November 2007 edit undo Ironwolf (talk \| contribs) 304 edits No edit summary Next edit →
Line 1:		Line 1:
	{{otheruses4\|the programming language\|self-taught individuals\|~~Autodidact~~}}		{{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.