Lemma Discovery and Strategies for Automated Induction

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Lemma Discovery and Strategies for Automated Induction

Popis výsledku v původním jazyce

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)

Název v anglickém jazyce

Lemma Discovery and Strategies for Automated Induction

Popis výsledku anglicky

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)

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA24-12759S" target="_blank" >GA24-12759S: Tvárné architektury pro automatické dokazování vět</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2024

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Automated Reasoning

ISBN

978-3-031-63498-7

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

19

Strana od-do

214-232

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Nancy

Datum konání akce

1. 7. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001273489700013