General description

Russell is a language for pure mathematics, built upon a metamath (www.metamath.org) language as a high level superstructure and supports fully automatic proving facility.

Formerly this language was called mdl, which stands for acronym for "Mathematics Development Language".

In fact, mdl program is a prover and a compiler from a relatively high-level language for the representation of formal mathematics to the simple and robust for checking language metamath.

Contents of the package

The latest tar.gz source package may be downloaded here: mdl-0.8.9-17.tar.gz
The package contains three programs:
  • mdl : the mdl prover and the compiler from mdl language to metamath.
  • mm : the decompiler from metamath to mdl.
  • metamath : original metamath checker, with two language restrictions switched off:
    • hypothesis labels are alowed to be not unique
    • expressions are alowed to start with a variable
  • smm : the verifier for the smm language (simplified metamath)
Also package contains extensive theorem basis math.mm (metamath base), which includes propositional logic, predicate logic, set theory, number systems (natural, rational, real, complex, etc.) and much more.

Quick installation

For installation instructions read INSTALL file in the package.

Simple installation: type './configure && make && make install'

System requirements

Full translation tests demand not less then 1Gb of RAM, not less then 150 Mb of free space on the hard disk.

Test scripts

Test scripts may be run to test the system and to obtain working mdl math library from the original metamath library. To run tests first compile mdl, mm, smm and metamath with the command './configure && make'. Then go to the directory 'math' and run appropriate script.