12. MoMM

MoMM is a matching, interreduction and database tool, downloadable from http://kti.ms.mff.cuni.cz/~urban/MoMM/MoMM.tar.gz.

It can load all of the Mizar theorems - now about 60000 clauses taking about 120M RAM - and tell you very quickly, if a claim you try to prove is subsumed by any of them.

Besides, there are about 700000 clauses created by logically correct generalization of all of the simple facts (simple justifications) ever proved by Mizar, that can additionally be loaded and used in exactly the same manner.

MoMM is based on Stephan Schulz's CLIB theorem proving library, available at http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html, making use of its very efficient implementation and indexing, and adding Mizar-specific features.

Modified verifier (`tptpver') generating MoMM problems from *4 errors (inferences rejected by the Mizar checker) is available in the MoMM distribution.

You can also add your own articles to the database used by MoMM for the matching, using the MoMM exporter (`tptpexp') and the additional `relcprem' tool from the MoMM distribution.

12.1 Installing MoMM

Download from http://kti.ms.mff.cuni.cz/~urban/MoMM/MoMM.tar.gz, and unpack the archive into the directory `$MIZFILES/MoMM'.

If it is not possible for you, unpack to arbitrary directory, and then set the Mizar Mode variable mizar-momm-dir.

That's all.

User Option: mizar-momm-dir

Directory containing the MoMM distribution.

The default value is "/usr/local/share/mizar/MoMM/".

12.2 Starting MoMM in Mizar Mode

To be able to use MoMM, you have to start it and load it with examples from other MML articles. Several functions and variables controlling this are described here, the most useful are available from menu.

User Option: mizar-use-momm

If t, errors *4 are clickable, trying to get MoMM's hints.
MoMM should be installed for this.

The default value is nil.

User Option: mizar-momm-load-tptp

If t, the simple justification clause bases are loaded into MoMM too.

The default value is t.

Command: mizar-run-momm-default &optional aname thsdirs tptp

Run MoMM for article aname.
Load theorems from all its directive filenames. If thsdirs is non-nil, use the theorem directive only. Complete typetable is loaded, which makes later on demand loading with `mizar-momm-add-files' possible. Use tptp to load the tptp files (non-theorem information) too.

Command: mizar-run-momm

Get type, clause and termbank files for running MoMM and run it.
Default process filter is used. Verify that the default argument files exist first.

Command: mizar-momm-add-files tlist &optional tptp

Add ths files from tlist into running MoMM.
The type-table must be loaded on start, e.g. by running MoMM with all.typ. If tptp, load tptp files too. Current directory is searched first, then the MoMM db.

Command: mizar-run-momm-full

Fast load MoMM with the full theorems db.
This takes about 120m in MoMM 0.2.

12.3 Getting MoMM hints

<S-down-mouse-3>

mizar-ask-momm

After starting MoMM, you can use it to get hints for formulas rejected by the checker (formulas that gave *4 errors).

The *4 errors become clickable with <S-down-mouse-3>, and MoMM's results are shown in the buffer *MoMM's Hints*.

Command: mizar-ask-momm event

Ask MoMM for hints on an error at click event.
The results are put into the buffer *MoMM's Hints*.