rentsch@unc.UUCP (Tim Rentsch) (09/25/84)
AutoMath is a tool for proof verification. The idea is to take a proof and write it in a very formal way, so that the mechanisms used in the proof can be mechanically verified. This is done using a type-checking scheme similar in concept to those used in modern programming languages. For references, the mathematician N. G. DeBruijn would be a good place to start. cheers, Tim
mark@gymble.UUCP (Mark Weiser) (09/25/84)
What is AutoMath? What I know is, it is some wort of automatically
verifiable mathematical notation, in which an entire textbook
has been written and automatically verified.
Anyone know more? Like, what is different that makes it verifiable?
What does the verification? How and for how much is it available?
How general is it?
--
Spoken: Mark Weiser ARPA: mark@maryland
CSNet: mark@umcp-cs UUCP: {seismo,allegra}!umcp-cs!markstevens@uiucdcs.UUCP (09/27/84)
As I recall AutoMath did not live up to the expectations of the original authors.. In particular the ability to Automatically Verify proofs of any complexity proved very difficult. I also do not believe the original research project continued much beyond the late 70's. --rick