MU's Architecture
The mathematics text to be learned is first translated by hand into FEL. This FEL text forms the input to MU. MU parses the FEL text and converts it into a frame like representation. This is then converted into features and is stored in the CMS using the features to index the result. The parsed data is fed into the proof checker and problem solver which uses the knowledge it has already acquired (and stored in the CMS) to try to explain the proofs, and solve the simple problems.