E-MaLeS 1.1

Daniel Kühlwein, Stephan Schulz, and Josef Urban


Picking the right search strategy is important for the success of
automatic theorem provers. E-MaLeS is a meta-system that uses machine
learning and strategy scheduling to optimize the performance of the
first-order theorem prover E. E-MaLeS applies a kernel-based learning
method to predict the run-time of a strategy on a given problem and
dynamically constructs a schedule of multiple promising strategies
that are tried in sequence on the problem. This approach has
significantly improved the performance of E 1.6, resulting in the
second place of E-MaLeS 1.1 in the FOF divisions of CASC-J6 and
CASC@Turing.