22/12/01 17:14:53.52 kl2o24qP.net
>>291
つづき
URLﾘﾝｸ(en.wikipedia.org)
Automath
Automath ("automating mathematics") is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correct