Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00381421" target="_blank" >RIV/68407700:21730/24:00381421 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.29007/sd6t" target="_blank" >https://doi.org/10.29007/sd6t</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.29007/sd6t" target="_blank" >10.29007/sd6t</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery

Popis výsledku v původním jazyce

While many of the state-of-art Automated Theorem Provers (ATP) like E and Vampire, were subject to extensive tuning of strategy schedules in the last decade, the classical ATP prover Prover9 has never been optimized in this direction. Both E and Vampire provide the user with an automatic mode to select good proof search strategies based on the properties of the input problem, while Prover9 provides by default only a relatively weak auto mode. Interestingly, Prover9 provides more varied means for proof control than its competitors. These means, however, must be manually investigated and that is possible only by experienced Prover9 users with a good understanding of how Prover9 works. In this paper, we investigate the possibilities of automatic configuration of Prover9 for user-specified benchmark problems. We employ the automated strategy invention systém Grackle to generate Prover9 strategies with both basic and advanced proof search options which require sophisticated strategy space features for Grac

Název v anglickém jazyce

Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery

Popis výsledku anglicky

While many of the state-of-art Automated Theorem Provers (ATP) like E and Vampire, were subject to extensive tuning of strategy schedules in the last decade, the classical ATP prover Prover9 has never been optimized in this direction. Both E and Vampire provide the user with an automatic mode to select good proof search strategies based on the properties of the input problem, while Prover9 provides by default only a relatively weak auto mode. Interestingly, Prover9 provides more varied means for proof control than its competitors. These means, however, must be manually investigated and that is possible only by experienced Prover9 users with a good understanding of how Prover9 works. In this paper, we investigate the possibilities of automatic configuration of Prover9 for user-specified benchmark problems. We employ the automated strategy invention systém Grackle to generate Prover9 strategies with both basic and advanced proof search options which require sophisticated strategy space features for Grac

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/LL1902" target="_blank" >LL1902: Obohacování SMT řešičů pomocí strojového učení</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

LPAR 2024: 25TH CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING

ISBN

—

ISSN

2398-7340

e-ISSN

2398-7340

Počet stran výsledku

9

Strana od-do

360-368

Název nakladatele

EasyChair Publications

Místo vydání

Manchester

Místo konání akce

Balaclava

Datum konání akce

26. 5. 2024

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

WRD - Celosvětová akce

Kód UT WoS článku

—