A survey of axiom selection as a machine learning problem

PorJosé A. Alonso

Se ha publicado un artículo automatización del razonamiento en Isabelle/HOL titulado A survey of axiom selection as a machine learning problem.

Sus autores son

Su resumen es

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.