ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback

Bartosz Piotrowski, Josef Urban

ATPboost is a system for solving sets of large-theory problems by interleaving ATP runs with state-of-the-art machine learning of premise selection from the proofs. Unlike many pre…