GRUNGE: A Grand Unified ATP Challenge

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F19%3A00337655" target="_blank" >RIV/68407700:21730/19:00337655 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-29436-6_8" target="_blank" >https://doi.org/10.1007/978-3-030-29436-6_8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-29436-6_8" target="_blank" >10.1007/978-3-030-29436-6_8</a>

Jazyk výsledku

angličtina

Název v původním jazyce

GRUNGE: A Grand Unified ATP Challenge

Popis výsledku v původním jazyce

This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possibly with types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formalisms on corresponding problems, and compare their performances. This also results in a new “grand unified” large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple formalisms in complementary ways, and jointly learn from the accumulated knowledge.

Název v anglickém jazyce

GRUNGE: A Grand Unified ATP Challenge

Popis výsledku anglicky

This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possibly with types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formalisms on corresponding problems, and compare their performances. This also results in a new “grand unified” large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple formalisms in complementary ways, and jointly learn from the accumulated knowledge.

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

<a href="/cs/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Umělá inteligence a uvažování</a><br>

Návaznosti

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

Rok uplatnění

2019

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 Deduction – CADE 27

ISBN

978-3-030-29435-9

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

19

Strana od-do

123-141

Název nakladatele

Springer, Cham

Místo vydání

—

Místo konání akce

Natal

Datum konání akce

27. 8. 2019

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

WRD - Celosvětová akce

Kód UT WoS článku

000693450800008