|
Vestnik Novosibirskogo Gosudarstvennogo Universiteta. Seriya Matematika, Mekhanika, Informatika, 2012, Volume 12, Issue 2, Pages 13–25
(Mi vngu115)
|
|
|
|
Smm, the simpefied metamath
D. Yu. Vlasovab a Novosibirsk State University, Novosibirsk, Russia
b Sobolev Institute of Mathematics, Siberian Branch of the Russian Academy of Sciences, Novosibirsk, Russia
Abstract:
Smm is a computer language for the formal mathematics, which is intended to represent the modern mathematics on a formal level and provide trustworthy proof verification of proofs. Smm is a simplified version of the language metamath. The syntax and semantics of smm are described.
Keywords:
formal mathematics, presentation of mathematical knowledge, automated proof checking.
Received: 26.03.2010
Citation:
D. Yu. Vlasov, “Smm, the simpefied metamath”, Vestn. Novosib. Gos. Univ., Ser. Mat. Mekh. Inform., 12:2 (2012), 13–25
Linking options:
https://www.mathnet.ru/eng/vngu115 https://www.mathnet.ru/eng/vngu/v12/i2/p13
|
Statistics & downloads: |
Abstract page: | 238 | Full-text PDF : | 90 | References: | 71 | First page: | 12 |
|