Lemma Discovery and Strategies for Automated Induction
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00381343" target="_blank" >RIV/68407700:21730/24:00381343 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1007/978-3-031-63498-7_13" target="_blank" >https://doi.org/10.1007/978-3-031-63498-7_13</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-63498-7_13" target="_blank" >10.1007/978-3-031-63498-7_13</a>
Alternative languages
Result language
angličtina
Original language name
Lemma Discovery and Strategies for Automated Induction
Original language description
We investigate how the automated inductive proof capabilities of the first-order prover Vampire can be improved by adding lemmas conjectured by the QuickSpec theory exploration system and by training strategy schedules specialized for inductive proofs. We find that adding lemmas improves performance (measured in number of proofs found for benchmark problems) by 40% compared to Vampire’s plain structural induction as baseline. Strategy training alone increases the number of proofs found by 130%, and the two methods in combination provide an increase of 183%. By combining strategy training and lemma discovery we can prove more inductive benchmarks than previous state-of-the-art inductive proof systems (HipSpec and CVC4)
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA24-12759S" target="_blank" >GA24-12759S: Malleable Theorem Proving Architectures</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2024
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
Automated Reasoning
ISBN
978-3-031-63498-7
ISSN
0302-9743
e-ISSN
1611-3349
Number of pages
19
Pages from-to
214-232
Publisher name
Springer
Place of publication
Cham
Event location
Nancy
Event date
Jul 1, 2024
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
001273489700013