id: 06055320
dt: j
an: 06055320
au: Vlasov, D.Yu.
ti: The language of formal mathematics Russell.
so: Vestn. Novosib. Gos. Univ., Ser. Mat. Mekh. Inform. 11, No. 2, 27-50
    (2011).
py: 2011
pu: Novosibirskij Gosuniversitet, Novosibirsk
la: RU
cc: 
ut: formal mathematics; automated reasoning; presentation of mathematical
    knowledge; automated proof checking; Russell
ci: 
li: 
ab: 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.
rv: