M(ost|uch) of M(izar|ath) Matches (MoMM)

• MoMM is a matching, interreduction and database tool for mathematical databases, optimized for Mizar, the description is at http://kti.mff.cuni.cz/~urban/MoMM/momm.ps, presentation is at MoMMPresentation
• the distribution is at http://kti.ms.mff.cuni.cz/~urban/MoMM/MoMM.tar.gz, the old version 0.1 is at http://kti.ms.mff.cuni.cz/~urban/MoMM/MoMM.tar.gz.v1
• one of its main uses is to help authors of Mizar articles, you need at least version 1.32 of MizarMode for that, version 1.33 contains support for additions in MoMM 0.2
• it is based on Stephan Schulz's CLIB http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html, you need version 0.62 of CLIB to compile MoMM 0.1 and vesrion 0.7 of CLIB to compile MoMM 0.2

TODO:

• The treatment of existential variables is a bit hacked now. Bill McCune^? has pointed to Champeaux's procedure (the paper attached here), however it requires (anti)skolemization for each pair of tested formulas, so I'll have to think how to do efficient indexing (possibly cheaply in E) for this. The procedure however seems directly usable instead of the Mizar Unifier (see AndrzejTrybulec^?'s description of that at http://www.cs.ru.nl/~freek/mizar/by.ps.gz).

• Champeaux.pdf: Champeaux's paper