Regularization in Spider-Style Strategy Discovery and Schedule Construction

Kód výsledku v IS VaVaI

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

Nalezeny alternativní kódy

RIV/68407700:21230/24:00376642

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-031-63498-7_12" target="_blank" >https://doi.org/10.1007/978-3-031-63498-7_12</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-63498-7_12" target="_blank" >10.1007/978-3-031-63498-7_12</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Regularization in Spider-Style Strategy Discovery and Schedule Construction

Popis výsledku v původním jazyce

To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given problem. In this paper, we report on a large-scale experiment with discovering strategies for the Vampire prover, targeting the FOF fragment of the TPTP library and constructing a schedule for it, based on the ideas of Andrei Voronkov’s system Spider. We examine the process from various angles, discuss the difficulty (or ease) of obtaining a strong Vampire schedule for the CASC competition, and establish how well a schedule can be expected to generalize to unseen problems and what factors influence this property.

Název v anglickém jazyce

Regularization in Spider-Style Strategy Discovery and Schedule Construction

Popis výsledku anglicky

To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given problem. In this paper, we report on a large-scale experiment with discovering strategies for the Vampire prover, targeting the FOF fragment of the TPTP library and constructing a schedule for it, based on the ideas of Andrei Voronkov’s system Spider. We examine the process from various angles, discuss the difficulty (or ease) of obtaining a strong Vampire schedule for the CASC competition, and establish how well a schedule can be expected to generalize to unseen problems and what factors influence this property.

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

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

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

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

20

Strana od-do

194-213

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

001273489700012