Selecting the selection

Kryštof Hoder, Giles Reger*, Martin Suda, Andrei Voronkov

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationAutomated Reasoning - 8th International Joint Conference, IJCAR 2016, Proceedings
EditorsNicola Olivetti, Ashish Tiwari
PublisherSpringer Nature
Pages313-329
Number of pages17
ISBN (Print)9783319402284
DOIs
Publication statusPublished - 12 Jun 2016
Event8th International Joint Conference on Automated Reasoning, IJCAR 2016 - Coimbra, Portugal
Duration: 27 Jun 20162 Jul 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9706
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th International Joint Conference on Automated Reasoning, IJCAR 2016
Country/TerritoryPortugal
CityCoimbra
Period27/06/162/07/16

Fingerprint

Dive into the research topics of 'Selecting the selection'. Together they form a unique fingerprint.

Cite this