MoMM
MoMM (in the narrower sense) is a tool allowing fast interreduction of a high number of clauses, dumping and fast-loading of the interreduced clause sets, and their use for real-time retrieval of matching clauses in an interactive mode. MoMM’s main task is now providing these services for the world’s largest body of formalized mathematics - the Mizar Mathematical Library (MML), which uses a richer formalism than just pure predicate logic. This task leads to a number of features (strength, speed, memory efficiency, dealing with the richer Mizar logic, etc.) required from MoMM, and we describe the choices taken in its implementation corresponding to these requirements. An important part of MoMM (in the wider sense) are the tools exporting the richer logic of MML into the clause-like format suitable for fast interreduction, and the tools allowing the use of MoMM as an interactive advisor for the authors of Mizar articles. These tools and choices taken in their implementation are also described here. Next we present some results of the interreduction of MML, which provide an interesting information about subsumption and repetition in the MML and can be used for its refactoring. This interreduction reveals that more than 2 percent of the main MML theorems are subsumed by others, and that for more than 50 percent of the internal lemmas proved by Mizar authors MoMM can provide a useful advice for their justification. Finally some problems and possible future work are discussed.
Keywords for this software
References in zbMATH (referenced in 22 articles )
Showing results 1 to 20 of 22.
Sorted by year (- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
- Caminati, Marco Bright; Rosolini, Giuseppe: Custom automations in Mizar (2013)
- Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef: The Mizar Mathematical Library in OMDoc: translation and applications (2013)
- Kaliszyk, Cezary; Urban, Josef: Automated reasoning service for HOL light (2013)
- Alama, Jesse; Mamane, Lionel; Urban, Josef: Dependencies in formal mathematics: applications and extraction for Coq and Mizar (2012)
- Rabe, Florian: A query language for formal mathematical libraries (2012)
- Lange, Christoph: Enabling collaboration on semiformal mathematical knowledge by semantic web integration (2011)
- Dietrich, Dominik; Schulz, Ewaryst: Crystal: Integrating structured queries into a tactic language (2010)
- Grabowski, Adam; Schwarzweller, Christoph: On duplication in mathematical repositories (2010)
- Cairns, Paul; Gow, Jeremy: Integrating searching and authoring in Mizar (2007)
- Grabowski, Adam; Schwarzweller, Christoph: Revisions as an essential tool to maintain mathematical repositories (2007)
- Urban, Josef; Bancerek, Grzegorz: Presenting and explaining mizar. (2007)
- Bancerek, Grzegorz: Information retrieval and rendering with MML Query (2006)
- Libbrecht, Paul; Melis, Erica: Methods to access and retrieve mathematical content in ActiveMath (2006)
- Urban, Josef: MPTP 0.2: Design, implementation, and initial experiments (2006)
- Urban, Josef: MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics (2006)
- Urban, Josef: XML-izing Mizar: Making semantic processing and presentation of MML easy (2006)