A Survey of Axiom Selection as a Machine Learning Problem

Abstract. 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 algo-rithms 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.