Selecting the Selection
Giles Reger, Martin Suda, Andrei Voronkov, Krystof Hoder

TL;DR
This paper introduces lookahead and incomplete literal selection strategies in saturation-based theorem proving, demonstrating their effectiveness in solving complex problems more efficiently.
Contribution
It proposes the novel concept of lookahead selection and advocates for incomplete selection functions to improve proof search in theorem provers.
Findings
Lookahead selection improves proof search efficiency.
Incomplete selection functions help solve previously unsolvable problems.
Experimental results show significant performance gains in Vampire.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge
