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 (onestep) 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; Flyspeck; TPTP; HOL Light; SPASS; MaLeCoP; MaSh; Coq; BliStr; OTTER; MizarMode; HOLyHammer; Isabelle; Isabelle/HOL 
Referenced in:  26 Publications 
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH  Year 

MPTPmotivation, implementation, first experiments. Zbl 1075.68081 Urban, Josef 
2004

all
top 5
Referenced by 27 Authors
Referenced 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 
Referenced in 2 Fields
26  Computer science (68XX) 
2  Mathematical logic and foundations (03XX) 