ENIGMAWatch: ProofWatch Meets ENIGMA

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F19%3A00339860" target="_blank" >RIV/68407700:21230/19:00339860 - isvavai.cz</a>

Nalezeny alternativní kódy

RIV/68407700:21730/19:00339860

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-030-29026-9_21" target="_blank" >https://doi.org/10.1007/978-3-030-29026-9_21</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-29026-9_21" target="_blank" >10.1007/978-3-030-29026-9_21</a>

Jazyk výsledku

angličtina

Název v původním jazyce

ENIGMAWatch: ProofWatch Meets ENIGMA

Popis výsledku v původním jazyce

In this work we describe a new learning-based proof guidance – ENIGMAWatch – for saturation-style first-order theorem provers. ENIGMAWatch combines two guiding approaches for the given-clause selection implemented for the E ATP system: ProofWatch and ENIGMA. ProofWatch is motivated by the watchlist (hints) method and based on symbolic matching of multiple related proofs, while ENIGMA is based on statistical machine learning. The two methods are combined by using the evolving information about symbolic proof matching as additional characterization of the saturation-style proof search for the statistical learning methods. The new system is evaluated on a large set of problems from the Mizar library. We show that the added proof-matching information is considered important by the statistical machine learners, and that it leads to improved performance over ProofWatch and ENIGMA.

Název v anglickém jazyce

ENIGMAWatch: ProofWatch Meets ENIGMA

Popis výsledku anglicky

In this work we describe a new learning-based proof guidance – ENIGMAWatch – for saturation-style first-order theorem provers. ENIGMAWatch combines two guiding approaches for the given-clause selection implemented for the E ATP system: ProofWatch and ENIGMA. ProofWatch is motivated by the watchlist (hints) method and based on symbolic matching of multiple related proofs, while ENIGMA is based on statistical machine learning. The two methods are combined by using the evolving information about symbolic proof matching as additional characterization of the saturation-style proof search for the statistical learning methods. The new system is evaluated on a large set of problems from the Mizar library. We show that the added proof-matching information is considered important by the statistical machine learners, and that it leads to improved performance over ProofWatch and ENIGMA.

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

ISBN

978-3-030-29025-2

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

15

Strana od-do

374-388

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

London

Datum konání akce

3. 9. 2019

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

WRD - Celosvětová akce

Kód UT WoS článku

—