@inproceedings{cd5d9eac59994d67901c50afc872597a,
title = "Selecting the selection",
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 of selecting a particular literal on the number of immediate children of the given clause and selects to minimize this value. There is also a case made for the use of incomplete selection strategies 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.",
author = "Kry{\v s}tof Hoder and Giles Reger and Martin Suda and Andrei Voronkov",
year = "2016",
month = jun,
day = "12",
doi = "10.1007/978-3-319-40229-1_22",
language = "English",
isbn = "9783319402284",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Nature",
pages = "313--329",
editor = "Nicola Olivetti and Ashish Tiwari",
booktitle = "Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings",
address = "United States",
note = "8th International Joint Conference on Automated Reasoning, IJCAR 2016 ; Conference date: 27-06-2016 Through 02-07-2016",
}