Regularization in Spider-Style Strategy Discovery and Schedule Construction
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917716015710208 |
|---|---|
| author | Bártek, Filip Chvalovský, Karel Suda, Martin |
| author_facet | Bártek, Filip Chvalovský, Karel Suda, Martin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_12869 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Regularization in Spider-Style Strategy Discovery and Schedule Construction Bártek, Filip Chvalovský, Karel Suda, Martin Artificial Intelligence Logic in Computer Science 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. |
| title | Regularization in Spider-Style Strategy Discovery and Schedule Construction |
| topic | Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2403.12869 |