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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alama, J., Heskes, T., Kühlwein, D., Tsivtsivadze, E., Urban, J.: Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. CoRR abs/1108.3446 (2011); Accepted to JAR
Armando, A., Baumgartner, P., Dowek, G. (eds.): IJCAR 2008. LNCS (LNAI), vol. 5195. Springer, Heidelberg (2008)
Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 116–130. Springer, Heidelberg (2011)
Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic Proof and Disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 12–27. Springer, Heidelberg (2011)
Korovin, K.: iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). Armando et al. [2], 292–298
de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2-3), 91–110 (2002)
Schulz, S.: E - A Brainiac Theorem Prover. AI Commun. 15(2-3), 111–126 (2002)
Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, New York (2004)
Sörensson, N., Eén, N.: MiniSat 2.1 and MiniSat++ 1.0 SAT Race, Editions Technical Report, Chalmers University of Technology, Sweden (2008)
Stenz, G., Wolf, A.: E-SETHEO: An Automated3 Theorem Prover – System Abstract. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 436–440. Springer, Heidelberg (2000)
Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4), 337–362 (2009)
Tammet, T.: Gandalf. Journal of Automated Reasoning 18, 199–204 (1997)
Urban, J.: MPTP 0.2: Design, Implementation, and Initial Experiments. J. Autom. Reasoning 37(1-2), 21–43 (2006)
Urban, J., Sutcliffe, G., Pudlák, P., Vyskocil, J.: MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidanc. In: Armando et al. [2], pp. 441–456
Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT. J. Artif. Int. Res. 32(1), 565–606 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kühlwein, D., Schulz, S., Urban, J. (2013). E-MaLeS 1.1. In: Bonacina, M.P. (eds) Automated Deduction – CADE-24. CADE 2013. Lecture Notes in Computer Science(), vol 7898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38574-2_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-38574-2_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38573-5
Online ISBN: 978-3-642-38574-2
eBook Packages: Computer ScienceComputer Science (R0)