Regularization in Spider-Style Strategy Discovery and Schedule Construction
The result's identifiers
Result code in 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>
Alternative codes found
RIV/68407700:21230/24:00376642
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Regularization in Spider-Style Strategy Discovery and Schedule Construction
Original language description
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.
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
Result was created during the realization of more than one project. More information in the Projects tab.
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-63497-0
ISSN
0302-9743
e-ISSN
1611-3349
Number of pages
20
Pages from-to
194-213
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
001273489700012