E-MaLeS 1.1

Daniel Kühlwein¹, Stephan Schulz², and Josef Urban¹

¹Radboud University Nijmegen, Nijmegen, Netherlands

²Technische Universität München, München, Germany

Abstract. 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.

LNAI 7898, p. 407 ff.

Full article in PDF | BibTeX

lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013