Solving Hard Mizar Problems with Instantiation and Strategy Invention
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F24%3A00379755" target="_blank" >RIV/68407700:21730/24:00379755 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1007/978-3-031-66997-2_18" target="_blank" >https://doi.org/10.1007/978-3-031-66997-2_18</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-66997-2_18" target="_blank" >10.1007/978-3-031-66997-2_18</a>
Alternative languages
Result language
angličtina
Original language name
Solving Hard Mizar Problems with Instantiation and Strategy Invention
Original language description
In this work, we prove over 3000 previously ATP-unproved Mizar/MPTP problems by using several ATP and AI methods, raising the number of ATP-solved Mizar problems from 75% to above 80%. First, we start to experiment with the cvc5 SMT solver which uses several instantiation-based heuristics that differ from the superposition-based systems, that were previously applied to Mizar, and add many new solutions. Then we use automated strategy invention to develop cvc5 strategies that largely improve cvc5's performance on the hard problems. In particular, the best invented strategy solves over 14% more problems than the best previously available cvc5 strategy. We also show that different clausification methods have a high impact on such instantiation-based methods, again producing many new solutions. In total, the methods solve 3,021 (21.3%) of the 14,163 previously unsolved hard Mizar problems. This is a new milestone over the Mizar large-theory benchmark and a large strengthening of the hammer methods for Mizar.
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
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2024
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
Intelligent Computer Mathematics
ISBN
978-3-031-66996-5
ISSN
0302-9743
e-ISSN
1611-3349
Number of pages
19
Pages from-to
315-333
Publisher name
Springer, Cham
Place of publication
—
Event location
Montréal, Québec
Event date
Aug 5, 2024
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
001292779800018