The language of formal mathematics Russell. (Russian. English summary) Zbl 1249.03006

Vlasov, D. Yu.

Vestn. Novosib. Gos. Univ., Ser. Mat. Mekh. Inform. 11, No. 2, 27-50 (2011).

Summary: Russell is a computer language for formal mathematics which is intended to represent modern mathematics on a formal level and to provide trustworthy proof verification and automation of routine (technical) proofs. Russell is a high-level superstructure language over the smm language, which, in turn, is a simplified version of the metamath language. The main features of Russell are: universality and reliability of metamath, human-readable and editable proof texts, which may be managed without external programs. Russell may be a candidate for the QED manifesto realization.

MSC:

03B35	Mechanization of proofs and logical operations
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30	Symbolic computation and algebraic computation

Keywords:

formal mathematics; automated reasoning; presentation of mathematical knowledge; automated proof checking; Russell

Software:

Russell; Smm; Metamath