Main features

Russell (named in honor of Bertrand Russell) is a logical framework for design and use of various formal calculi. It is pure, i.e. it is not based on any particular calculus, as opposed to some other logical frameworks (Twelf, MetaPRL, etc.). The implementation of Russell language is a translator from Russell source code to the simplified
metamath language, so Russell is not less trustworthy then metamath and may be concerned as a high-level language towards metamath. Russell presupposes the ability of the fully automatic proving, and current implementation of Russell supports it.

Leave a Reply

Your email address will not be published. Required fields are marked *