MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers
This work provides a tool for researchers and practitioners in automated reasoning to enhance theorem prover performance, though it is incremental as it builds on existing tuning methods.
The paper tackles the problem of automatically tuning automated theorem provers by introducing MaLeS, a framework that addresses both strategy finding and scheduling, resulting in an average improvement of 8.67% more problems solved compared to default settings.
MaLeS is an automatic tuning framework for automated theorem provers. It provides solutions for both the strategy finding as well as the strategy scheduling problem. This paper describes the tool and the methods used in it, and evaluates its performance on three automated theorem provers: E, LEO-II and Satallax. An evaluation on a subset of the TPTP library problems shows that on average a MaLeS-tuned prover solves 8.67% more problems than the prover with its default settings.