Urban, Josef; Hoder, Krystof; Voronkov, Andrei Evaluation of automated theorem proving on the Mizar mathematical library. (English) Zbl 1294.68128 Fukuda, Komei (ed.) et al., Mathematical software – ICMS 2010. Third international congress on mathematical software, Kobe, Japan, September 13–17, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-15581-9/pbk). Lecture Notes in Computer Science 6327, 155-166 (2010). Summary: This paper investigates the strength of first-order automatic theorem provers (ATPs) in proving theorems and lemmas from the Mizar proof assistant’s formal mathematical library. Several Mizar use-cases are described and evaluated, as well as various ATP systems and strategies. The new version of the leading Vampire ATP system is included in the evaluation, experiments with Mizar-specific strategy-selection are performed with E the prover, and the SInE axiom selection is evaluated on large Mizar problems with both E and Vampire. A rough mathematical division of the Mizar library is introduced, and the ATP performance is evaluated on it.For the entire collection see [Zbl 1196.68008]. Cited in 10 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Software:MML; VAMPIRE; Mizar; MPTP 0.2; MaLARea; E Theorem Prover PDFBibTeX XMLCite \textit{J. Urban} et al., Lect. Notes Comput. Sci. 6327, 155--166 (2010; Zbl 1294.68128) Full Text: DOI