Learning Theorem Proving Components

Karel Chvalovský, Jan Jakubův, Miroslav Olšák +1

Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selectio…