Parental Guidance in E ∗

Parents and Clause Selection in E State-of-the-art automated theorem provers (ATP), such as E [13, 14], Prover9 [10], and Vampire [11], are based on the saturation loop paradigm and the given clause algorithm [12]. The input problem in first-order logic is translated into a refutationally equivalent set of clauses. The ATP’s search for a contradiction maintains two sets of clauses: processed (initially empty) and unprocessed (initially the input clauses). At each step, one unprocessed clause is selected (given), and all of the possible inferences with all the processed clauses are generated (typically using resolution, paramodulation, etc.), extending the unprocessed clause set. The selected clause is then moved to the processed clause set. An important invariant is that all mutual inferences among the processed clauses have been computed at each step. The selection of the “right” given clause is known to be an important choice-point vital to the success of the proof search. E’s strategies consist of clause evaluation functions that weigh and prioritize clauses for selection based on their symbols and properties. The ENIGMA systems [2–7] apply various machine learning methods to learn how to select effective given clauses from corpora of previous successful proof searches. Given clause selection does not give the ENIGMA system complete control over the inferred clauses because all inferences between the given clause and clauses in the processed clause set are computed. One reason this can be important is that the ENIGMA systems tend to perform best when run in cooperation with a strong E strategy where each selects half the clauses. This talk discusses the implementation and experimentation of an ENIGMA system that can “judge children by their parents” to filter out unnecessary inferences between the given clause and processed clauses . It is hoped that pruning the children of irresponsible parents can improve E’s performance by allowing clause selection ENIGMA models and E strategies greater focus.