Evaluation of automated theorem proving on the Mizar mathematical library

Josef Urban; Krystof Hoder; Andrei Voronkov

doi:10.1007/978-3-642-15582-6_30

Evaluation of automated theorem proving on the Mizar mathematical library

Josef Urban, Krystof Hoder, Andrei Voronkov

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Pages	155-166
Number of pages	11
Volume	6327
DOIs	https://doi.org/10.1007/978-3-642-15582-6_30
Publication status	Published - 2010
Event	3rd International Congress on Mathematical Software, ICMS 2010 - Kobe Duration: 1 Jul 2010 → …

Conference

Conference	3rd International Congress on Mathematical Software, ICMS 2010
City	Kobe
Period	1/07/10 → …

Access to Document

10.1007/978-3-642-15582-6_30

Cite this

@inproceedings{f361c9e1cc704a3bb485f7ef52c1664d,

title = "Evaluation of automated theorem proving on the Mizar mathematical library",

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. {\textcopyright} 2010 Springer-Verlag.",

author = "Josef Urban and Krystof Hoder and Andrei Voronkov",

year = "2010",

doi = "10.1007/978-3-642-15582-6_30",

language = "English",

isbn = "3642155812",

volume = "6327",

pages = "155--166",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

note = "3rd International Congress on Mathematical Software, ICMS 2010 ; Conference date: 01-07-2010",

}

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)|Lect. Notes Comput. Sci.. vol. 6327, pp. 155-166, 3rd International Congress on Mathematical Software, ICMS 2010, Kobe, 1/07/10. https://doi.org/10.1007/978-3-642-15582-6_30

Evaluation of automated theorem proving on the Mizar mathematical library. / Urban, Josef; Hoder, Krystof; Voronkov, Andrei.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 6327 2010. p. 155-166.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Evaluation of automated theorem proving on the Mizar mathematical library

AU - Urban, Josef

AU - Hoder, Krystof

AU - Voronkov, Andrei

PY - 2010

Y1 - 2010

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

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

U2 - 10.1007/978-3-642-15582-6_30

DO - 10.1007/978-3-642-15582-6_30

M3 - Conference contribution

SN - 3642155812

SN - 9783642155819

VL - 6327

SP - 155

EP - 166

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

T2 - 3rd International Congress on Mathematical Software, ICMS 2010

Y2 - 1 July 2010

ER -

Evaluation of automated theorem proving on the Mizar mathematical library

Abstract

Conference

Access to Document

Fingerprint

Cite this