MPTP
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.
Keywords for this software
References in zbMATH (referenced in 21 articles , 1 standard article )
Showing results 1 to 20 of 21.
Sorted by year (- Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol: The role of the Mizar mathematical library for interactive proof development in Mizar (2018)
- Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef: TacticToe: learning to reason with HOL4 tactics (2017)
- Brown, Chad E.; Urban, Josef: Extracting higher-order goals from the Mizar Mathematical Library (2016)
- 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)
- Färber, Michael; Kaliszyk, Cezary: Random forests for premise selection (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)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (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)
- Urban, Josef; Vyskočil, Jiří: Theorem proving in large formal mathematics as an emerging AI field (2013)
- Urban, Josef; Sutcliffe, Geoff: ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (2008)
- Urban, Josef; Sutcliffe, Geoff; Pudlák, Petr; Vyskočil, Jiří: MaLARea SG1 -- machine learner for automated reasoning with semantic guidance (2008)
- Cairns, Paul; Gow, Jeremy: Integrating searching and authoring in Mizar (2007)
- Urban, Josef; Bancerek, Grzegorz: Presenting and explaining Mizar (2007)
- Urban, Josef; Sutcliffe, Geoff: ATP cross-verification of the Mizar MPTP challenge problems (2007)
- Urban, Josef: XML-izing Mizar: Making semantic processing and presentation of MML easy (2006)
- Urban, Josef: MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics (2006)
- Urban, Josef: MPTP 0.2: Design, implementation, and initial experiments (2006)
- Urban, Josef: MPTP-motivation, implementation, first experiments (2004)