Name
Abstract | ||
|---|---|---|
Smart premise selection is essential when using automated reasoning as a tool for large-theory formal proof development. This work develops learning-based premise selection in two ways. First, a fine-grained dependency analysis of existing high-level formal mathematical proofs is used to build a large knowledge base of proof dependencies, providing precise data for ATP-based re-verification and for training premise selection algorithms. Second, a new machine learning algorithm for premise selection based on kernel methods is proposed and implemented. To evaluate the impact of both techniques, a benchmark consisting of 2078 large-theory mathematical problems is constructed, extending the older MPTP Challenge benchmark. The combined effect of the techniques results in a 50 % improvement on the benchmark over the state-of-the-art Vampire/SInE system for automated reasoning in large theories. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/s10817-013-9286-5 | J. Autom. Reasoning |
Keywords | DocType | Volume |
Automated reasoning in large theories,Machine learning,Premise selection,Automated theorem proving | Journal | 52 |
Issue | ISSN | Citations |
2 | 0168-7433 | 32 |
PageRank | References | Authors |
1.22 | 29 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jesse Alama | 1 | 106 | 15.00 |
| Tom Heskes | 2 | 1519 | 198.44 |
| Daniel Kühlwein | 3 | 154 | 8.75 |
| Evgeni Tsivtsivadze | 4 | 179 | 12.61 |
| Josef Urban | 5 | 635 | 46.75 |