Paper Info
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.
Year
Venue
Keywords
2010
ICMS
rough mathematical division,mizar mathematical library,mizar-specific strategy-selection,atp performance,mizar use-cases,mizar library,mizar proof assistant,various atp system,large mizar problem,automated theorem,formal mathematical library,leading vampire atp system,intelligent systems
Field
DocType
Volume
Mizar system,Theorem provers,Axiom,Computer science,Automated theorem proving,Algorithm,Theoretical computer science,Gas meter prover,Calculus,Lemma (mathematics),Proof assistant
Conference
6327
ISSN
ISBN
Citations 
0302-9743
3-642-15581-2
20
PageRank 
References 
Authors
1.22
16
3
Name
Order
Citations
PageRank
Josef Urban163546.75
Kryštof Hoder2584.02
Andrei Voronkov32670225.46