Learning Theorem Proving Components

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F21%3A00353686" target="_blank" >RIV/68407700:21730/21:00353686 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-86059-2_16" target="_blank" >https://doi.org/10.1007/978-3-030-86059-2_16</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-86059-2_16" target="_blank" >10.1007/978-3-030-86059-2_16</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Learning Theorem Proving Components

Popis výsledku v původním jazyce

Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selection heuristics in such systems are, however, often evaluating clauses in isolation, ignoring other clauses. This has changed recently by equipping the E/ENIGMA system with a graph neural network (GNN) that chooses the next given clause based on its evaluation in the context of previously selected clauses. In this work, we describe several algorithms and experiments with ENIGMA, advancing the idea of contextual evaluation based on learning important components of the graph of clauses.

Název v anglickém jazyce

Learning Theorem Proving Components

Popis výsledku anglicky

Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selection heuristics in such systems are, however, often evaluating clauses in isolation, ignoring other clauses. This has changed recently by equipping the E/ENIGMA system with a graph neural network (GNN) that chooses the next given clause based on its evaluation in the context of previously selected clauses. In this work, we describe several algorithms and experiments with ENIGMA, advancing the idea of contextual evaluation based on learning important components of the graph of clauses.

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í

2021

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 with Analytic Tableaux and Related Methods

ISBN

978-3-030-86058-5

ISSN

0302-9743

e-ISSN

0302-9743

Počet stran výsledku

13

Strana od-do

266-278

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Birmingham

Datum konání akce

6. 9. 2021

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

WRD - Celosvětová akce

Kód UT WoS článku

000711656700016