Publications in Scientific Journals:
J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, J. Urban:
"Premise selection for mathematics by corpus analysis and kernel methods";
Journal of Automated Reasoning,
52
(2014),
2;
191
- 213.
English 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.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/s10817-013-9286-5
Created from the Publication Database of the Vienna University of Technology.