The language of formal mathematics Russell. 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.
Keywords for this software
References in zbMATH (referenced in 1 article , 1 standard article )
Showing result 1 of 1.