A Survey of Axiom Selection as a Machine Learning Problem
Daniel Kühlwein, Jasmin Christian Blanchette · Radboud Repository (Radboud University) · 2014
Automatic theorem provers struggle to discharge proof obligations of interactive theorem provers. This is partly due to the large number of background facts that are passed to the automatic provers as axioms. Axiom selection algorithms predict the relevance of facts, thereby helping to reduce the search space of automatic provers. This paper presents an introduction to axiom selection as a machine learning problem and describes the challenges that distinguish it from other applications of machine learning.