ENIGMAWatch: ProofWatch Meets ENIGMA
The result's identifiers
Result code in 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>
Alternative codes found
RIV/68407700:21730/19:00339860
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
ENIGMAWatch: ProofWatch Meets ENIGMA
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Artificial Intelligence and Reasoning</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2019
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Automated Reasoning with Analytic Tableaux and Related Methods
ISBN
978-3-030-29025-2
ISSN
0302-9743
e-ISSN
—
Number of pages
15
Pages from-to
374-388
Publisher name
Springer
Place of publication
Cham
Event location
London
Event date
Sep 3, 2019
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—