MPTP 0.2
MPTP 0.2: Design, implementation, and initial experiments This paper describes the second version of the Mizar Problems for Theorem Proving (MPTP) system and first experimental results obtained with it. The goal of the MPTP project is to make the large formal Mizar Mathematical Library (MML) available to current first-order automated theorem provers (ATPs) (and vice versa) and to boost the development of domain-based, knowledge-based, and generally AI-based ATP methods. This version of MPTP switches to a generic extended TPTP syntax that adds term-dependent sorts and abstract (Fraenkel) terms to the TPTP syntax. We describe these extensions and explain how they are transformed by MPTP to standard TPTP syntax using relativization of sorts and deanonymization of abstract terms. Full Mizar proofs are now exported and also encoded in the extended TPTP syntax, allowing a number of ATP experiments. This covers, for example, consistent handling of proof-local constants and proof-local lemmas and translating of a number of Mizar proof constructs into the TPTP formalism. The proofs using second-order Mizar schemes are now handled by the system, too, by remembering (and, if necessary, abstracting from the proof context) the first-order instances that were actually used. These features necessitated changes in Mizar, in the Mizar-to-TPTP exporter, and in the problem-creating tools. Mizar has been reimplemented to produce and use natively a detailed XML format, suitable for communication with other tools. The Mizar-to-TPTP exporter is now just a XSLT stylesheet translating the XML tree to the TPTP syntax. The problem creation and other MPTP processing tasks are now implemented in about 1,300 lines of Prolog. All these changes have made MPTP more generic, more complete, and more correct. The largest remaining issue is the handling of the Mizar arithmetical evaluations. We describe several initial ATP experiments, both on the easy and on the hard MML problems, sometimes assisted by machine learning. It is shown that on the nonarithmetical problems, countersatisfiability (completions) is no longer detected by the ATP systems, suggesting that the `Mizar deconstruction’ done by MPTP is in this case already complete. About every fifth nonarithmetical theorem is proved in a fully autonomous mode, in which the premises are selected by a machine-learning system trained on previous proofs. In 329 of these cases, the newly discovered proofs are shorter than the MML originals and therefore are likely to be used for MML refactoring. This situation suggests that even a simple inductive or deductive system trained on formal mathematics can be sometimes smarter than MML authors and usable for general discovery in mathematics.
Keywords for this software
References in zbMATH (referenced in 32 articles , 1 standard article )
Showing results 1 to 20 of 32.
Sorted by year (- Sutcliffe, Geoff: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0 (2017)
- Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
- Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
- Brown, Chad E.; Urban, Josef: Extracting higher-order goals from the Mizar Mathematical Library (2016)
- Jan Jakubuv, Josef Urban: BliStrTune: Hierarchical Invention of Theorem Proving Strategies (2016) arXiv
- Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol; Urban, Josef: Mizar: state-of-the-art and beyond (2015)
- Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias: Mining the Archive of Formal Proofs (2015)
- Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
- Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
- Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef: Premise selection for mathematics by corpus analysis and kernel methods (2014)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
- Alama, Jesse: Eliciting implicit assumptions of Mizar proofs by property omission (2013)
- Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef: The Mizar Mathematical Library in OMDoc: translation and applications (2013)
- Kühlwein, Daniel; Schulz, Stephan; Urban, Josef: E-MaLeS 1.1 (2013)
- Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff: ATP and presentation service for Mizar formalizations (2013)
- Urban, Josef; Vyskočil, Jiří: Theorem proving in large formal mathematics as an emerging AI field (2013)
- Alama, Jesse; Kühlwein, Daniel; Urban, Josef: Automated and human proofs in general mathematics: an initial comparison (2012)
- Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef: Licensing the Mizar Mathematical Library (MML) (2011)
- Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C.: Extending Sledgehammer with SMT solvers (2011)
- Hoder, Kryštof; Voronkov, Andrei: Sine qua non for large theory reasoning (2011)