| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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 | ||
| 12.2 Starting MoMM in Mizar Mode | ||
| 12.3 Getting MoMM hints |
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
Directory containing the MoMM distribution.
The default value is "$MIZFILES/MoMM/".
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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.
If t, errors *4 are clickable, trying to get MoMM’s hints.
MoMM should be installed for this.
The default value is nil.
If t, the simple justification clause bases are loaded into MoMM too.
The default value is t.
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.
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.
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.
Fast load MoMM with the full theorems db.
This takes about 120m in MoMM 0.2.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
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*.
Ask MoMM for hints on an error at click event.
The results are put into the buffer *MoMM’s Hints*.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated by Josef Urban on February 20, 2014 using texi2html 1.82.