×

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].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI