aut(ID:6969/aut047)
2002 version of AUTOMATH, compatible with AUT-QE and AUT-PI
written in C
Related languages
| AUTOMATH |
=> |
aut | |
Evolution of |
| AUT-QE |
=> |
aut | |
Incorporated some features of |
Resources - aut Home page, includes manual
Automath is a language designed by N.G. the Bruijn in the late sixties in order to represent mathematical proof in the computer. It's the direct ancestor of the "type theoretical" line of proof assistants from which the better known current ones are Nuprl and Coq.
This web page is the home of a modern reimplementation of Automath by Freek Wiedijk. It presents a portable, simple and fast checker (which is written in C) for the AUT-68 and AUT-QE languages.
external link
|