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 firstorder automated theorem provers (ATPs) (and vice versa) and to boost the development of domainbased, knowledgebased, and generally AIbased ATP methods. This version of MPTP switches to a generic extended TPTP syntax that adds termdependent 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 prooflocal constants and prooflocal lemmas and translating of a number of Mizar proof constructs into the TPTP formalism. The proofs using secondorder Mizar schemes are now handled by the system, too, by remembering (and, if necessary, abstracting from the proof context) the firstorder instances that were actually used. These features necessitated changes in Mizar, in the MizartoTPTP exporter, and in the problemcreating tools. Mizar has been reimplemented to produce and use natively a detailed XML format, suitable for communication with other tools. The MizartoTPTP 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 machinelearning 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.68095 Urban, Josef 
2006

all
top 5
Cited by 53 Authors
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 (68XX) 
5  Mathematical logic and foundations (03XX) 