MPTP 0.2 swMATH ID: 2589 Software Authors: Urban, Josef Description: 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. Homepage: https://github.com/JUrban/MPTP2 Source Code: https://github.com/JUrban/MPTP2 Keywords: Mizar Problems for Theorem Proving Related Software: Mizar; E Theorem Prover; VAMPIRE; TPTP; MaLARea; Isabelle/HOL; MML; Flyspeck; Sledgehammer; MPTP; SPASS; MoMM; HOL Light; OTTER; MaLeCoP; BliStr; z3; Coq; Isabelle; leanCoP Cited in: 51 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095Urban, Josef 2006 all top 5 Cited by 53 Authors 28 Urban, Josef 11 Kaliszyk, Cezary 9 Sutcliffe, Geoff 6 Blanchette, Jasmin Christian 5 Alama, Jesse 4 Böhme, Sascha 4 Jakubův, Jan 4 Kühlwein, Daniel 4 Pąk, Karol 4 Schulz, Stephan 3 Bancerek, Grzegorz 3 Chvalovský, Karel 3 Naumowicz, Adam 3 Rudnicki, Piotr 3 Vyskočil, Jiří 2 Byliński, Czesław 2 Goertzel, Zarathustra A. 2 Grabowski, Adam 2 Hoder, Kryštof 2 Kohlhase, Michael 2 Korniłowicz, Artur 2 Matuszewski, Roman 2 Nipkow, Tobias 2 Olšák, Miroslav 2 Paulson, Lawrence Charles 2 Popescu, Andrei 2 Rawson, Michael 2 Reger, Giles 2 Smallbone, Nicholas 2 Suda, Martin 2 Voronkov, Andrei 2 Wang, Qingxiang 1 Brown, Chad Edward 1 Gauthier, Thibault 1 Geuvers, Jan Herman 1 Greenaway, David 1 Haslbeck, Maximilian P. L. 1 Heskes, Tom M. 1 Holden, Edvard K. 1 Iancu, Mihnea 1 Irving, Geoffrey 1 Korovin, Konstantin 1 Loos, Sarah M. 1 Mamane, Lionel Elie 1 Matichuk, Daniel 1 Pease, Adam 1 Proroković, Krsto 1 Rabe, Florian 1 Schmidhuber, Jürgen 1 Szegedy, Christian 1 Tsivtsivadze, Evgeni 1 Wand, Michael 1 Wernhard, Christoph all top 5 Cited in 6 Serials 12 Journal of Automated Reasoning 1 Journal of Symbolic Computation 1 AI Communications 1 Mathematics in Computer Science 1 Logical Methods in Computer Science 1 Journal of Formalized Reasoning Cited in 2 Fields 51 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) Citations by Year