Abstract
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. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Urban, J., Hoder, K., & Voronkov, A. (2010). Evaluation of automated theorem proving on the Mizar mathematical library. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6327 LNCS, pp. 155–166). https://doi.org/10.1007/978-3-642-15582-6_30
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
