MPTP swMATH ID: 2489 Software Authors: Urban, Josef Description: We describe a number of new possibilities for current theorem provers, that arise with the existence of large integral bodies of formalized mathematics. Then we proceed to describe the implementation of the MPTP system, which makes the largest existing corpus of formalized mathematics available to theorem provers. MPTP (Mizar Problems for Theorem Proving) is a system for translating the Mizar Mathematical Library (MML) into untyped first order format suitable for automated theorem provers, and for generating theorem proving problems corresponding to MML. The first version generates about 30000 problems from complete proofs of Mizar theorems, and about 630000 problems from the simple (one-step) justifications done by the Mizar checker. We describe the design and structure of the system, the main problems encountered in this kind of system, their solutions, current limitations, and planned future extensions. We present results of first experiments with reproving the MPTP problems with theorem provers. We also describe first implementation of the Mizar Proof Advisor (MPA) used for selecting suitable axioms from the large library for an arbitrary problem, and again, present first results of this combined MPA/ATP architecture on MPTP. Homepage: http://wiki.mizar.org/twiki/bin/view/Mizar/MpTP Keywords: ATP; Mizar; MPA; MPTP Related Software: Mizar; E Theorem Prover; MaLARea; VAMPIRE; MPTP 0.2; MML; MoMM; TPTP; Flyspeck; HOL Light; SPASS; MaLeCoP; MizarMode; OTTER; MaSh; Coq; BliStr; Isabelle; HOLyHammer; Isabelle/HOL Cited in: 26 Documents Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year MPTP-motivation, implementation, first experiments. Zbl 1075.68081Urban, Josef 2004 all top 5 Cited by 27 Authors 21 Urban, Josef 9 Kaliszyk, Cezary 3 Bancerek, Grzegorz 3 Pąk, Karol 3 Sutcliffe, Geoff 3 Vyskočil, Jiří 2 Byliński, Czesław 2 Färber, Michael 2 Gauthier, Thibault 2 Grabowski, Adam 2 Korniłowicz, Artur 2 Matuszewski, Roman 2 Naumowicz, Adam 1 Alama, Jesse 1 Brown, Chad Edward 1 Cairns, Paul 1 Gow, Jeremy 1 Heskes, Tom M. 1 Jakubův, Jan 1 Kühlwein, Daniel 1 Kumar, Ramana 1 Norrish, Michael 1 Pudlák, Pavel 1 Rawson, Michael 1 Reger, Giles 1 Schulz, Stephan 1 Tsivtsivadze, Evgeni Cited in 5 Serials 10 Journal of Automated Reasoning 1 Journal of Symbolic Computation 1 AI Communications 1 Journal of Applied Logic 1 Mathematics in Computer Science Cited in 2 Fields 26 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year