Extending E Prover with Similarity Based Clause Selection Strategies
Result description
E prover is a state-of-the-art theorem prover for first-order logic with equality. E prover is built around a saturation loop, where new clauses are derived by inference rules from previously derived clauses. Selection of clauses for the inference provides the main source of non-determinism and an important choice-point of the loop where the right choice can dramatically influence the proof search. In this work we extend E Prover with several new clause selection strategies based on similarity of a clause with the conjecture. In particular, clauses which are more related to the conjecture are preferred. We implement different strategies that define the relationship with a conjecture in different ways. We provide an implementation of the proposed selection strategies and we evaluate their efficiency on an extensive benchmark set.
Keywords
TheoAutomated Theorem ProvingLarge Theory ReasoningClause Selection
The result's identifiers
Result code in IS VaVaI
Result on the web
DOI - Digital Object Identifier
Alternative languages
Result language
angličtina
Original language name
Extending E Prover with Similarity Based Clause Selection Strategies
Original language description
E prover is a state-of-the-art theorem prover for first-order logic with equality. E prover is built around a saturation loop, where new clauses are derived by inference rules from previously derived clauses. Selection of clauses for the inference provides the main source of non-determinism and an important choice-point of the loop where the right choice can dramatically influence the proof search. In this work we extend E Prover with several new clause selection strategies based on similarity of a clause with the conjecture. In particular, clauses which are more related to the conjecture are preferred. We implement different strategies that define the relationship with a conjecture in different ways. We provide an implementation of the proposed selection strategies and we evaluate their efficiency on an extensive benchmark set.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
—
Continuities
R - Projekt Ramcoveho programu EK
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Lecture Notes in Computer Science 9791
ISBN
978-3-319-42546-7
ISSN
0302-9743
e-ISSN
—
Number of pages
6
Pages from-to
151-156
Publisher name
Springer
Place of publication
Basel
Event location
Bialystok
Event date
Jul 25, 2016
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000389402700011
Basic information
Result type
D - Article in proceedings
CEP
IN - Informatics
Year of implementation
2016