Selecting the Selection
  Modern saturation-based Automated Theorem Provers typically implement the
superposition calculus for reasoning about first-order logic with or without
equality. Practical implementations of this calculus use a variety of literal
selections and term orderings to tame the growth of the search space and help
steer proof search. This paper introduces the notion of lookahead selection
that estimates (looks ahead) the effect on the search space of selecting a
literal. There is also a case made for the use of incomplete selection
functions that attempt to restrict the search space instead of satisfying some
completeness criteria. Experimental evaluation in the \Vampire\ theorem prover
shows that both lookahead selection and incomplete selection significantly
contribute to solving hard problems unsolvable by other methods.
