Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery

Result code in 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>

Result on the web

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

Result language

angličtina

Original language name

Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery

Original language description

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

Czech name

—

Czech description

—

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)

Project

<a href="/en/project/LL1902" target="_blank" >LL1902: Powering SMT Solvers by Machine Learning</a><br>

Continuities

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

Publication year

2024

Confidentiality

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

Article name in the collection

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

ISBN

—

ISSN

2398-7340

e-ISSN

2398-7340

Number of pages

9

Pages from-to

360-368

Publisher name

EasyChair Publications

Place of publication

Manchester

Event location

Balaclava

Event date

May 26, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—