D. Yu. Vlasov, “Smm, the simpefied metamath”, Vestn. Novosib. Gos. Univ., Ser. Mat. Mekh. Inform., 2012, Volume 12, Issue 2,Pages <nobr>13

Smm, the simpefied metamath

D. Yu. Vlasov^ab

^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.

UDC: 510.23+811.93

Received: 26.03.2010