Dataset-Specific Strategies for the E Theorem Prover

The E automated theorem proving system has an “automatic” mode that analyzes the input problem in order to choose an effective proof search strategy. A strategy includes the term/literal orderings, given clause selection heuristics, and a number of other parameters. This paper investigates the idea of creating one strategy for a given dataset of problems by merging the strategies chosen by E’s automatic mode over all of the problems in the dataset. This strategy merging approach is evaluated on the MPTPTP2078, VBT, and SLH-29 datasets. Surprisingly, the merged strategies outperform E’s automatic mode over all three datasets.