A Mathematical Benchmark for Inductive Theorem Provers

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F23%3A00372207" target="_blank" >RIV/68407700:21730/23:00372207 - isvavai.cz</a>

Výsledek na webu

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

DOI - Digital Object Identifier

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

Jazyk výsledku

angličtina

Název v původním jazyce

A Mathematical Benchmark for Inductive Theorem Provers

Popis výsledku v původním jazyce

We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectured by a learning-guided synthesis system using a language with looping operators. The operators implement recursion, and thus many of the proofs require induction on natural numbers. The benchmark contains problems of varying difficulty from a wide area of mathematical domains. We believe that these characteristics will make it an effective judge for the progress of inductive theorem provers in this domain for years to come.

Název v anglickém jazyce

A Mathematical Benchmark for Inductive Theorem Provers

Popis výsledku anglicky

We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectured by a learning-guided synthesis system using a language with looping operators. The operators implement recursion, and thus many of the proofs require induction on natural numbers. The benchmark contains problems of varying difficulty from a wide area of mathematical domains. We believe that these characteristics will make it an effective judge for the progress of inductive theorem provers in this domain for years to come.

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í

2023

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

Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)

ISBN

—

ISSN

2398-7340

e-ISSN

2398-7340

Počet stran výsledku

14

Strana od-do

224-237

Název nakladatele

EasyChair Publications

Místo vydání

Manchester

Místo konání akce

Manizales

Datum konání akce

4. 6. 2023

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

WRD - Celosvětová akce

Kód UT WoS článku

—