[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] MoMM:Most of Math Matches
- not yet ;-), now rather: MoMM:Much of Mizar Matches.
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 200M 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 generating MoMM problems from *4 errors (inferences
rejected by the Mizar checker) is available.
Authors of Mizar articles can load MoMM with customized theories, and
ask her to help them with the problems :-).
You will need updated Mizar mode for Emacs for this, which automates
the process of loading customized theories, and makes *4 errors
clickable (it is in the CVS).
MoMM is now compiled for Linux only, compilation on less sane platforms
is left to their unlucky users. I can help them by running completely
loaded MoMM as a web service, if someone provides a server with
1-2G RAM to do this on (MoMM:Most of Memory Misused :-). Let me know
if you are interested.
MoMM is version 0.1 and consists of several tools. There are many
features I would like to add, some bugs I am aware of, and most
probably many bugs I do not know about. Let me know if you find any.
Some doc should be eventually generated at
http://alioth.uwb.edu.pl/twiki/bin/view/Mizar/MoMM .
As of now, the interreduction revealed about 1200 redundant clauses
among those generated from Mizar theorems (this does not mean there
are 1200 redundant theorems in MML). The redundancy in clauses
generated from simple justifications has not been measured on the
whole MML yet, preliminary estimate is about 40% redundancy.
Josef