ENIGMA: Efficient Learning-based Inference Guiding Machine

Jan Jakubův, Josef Urban

ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many proof searches are classified as positive and negative b…