2 citations · 2 across the 5 of their papers we have counts for
5 papers
Solving Hard Mizar Problems with Instantiation and Strategy Invention
Jan Jakubův, Mikoláš Janota, Josef Urban
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…
MizAR 60 for Mizar 50
Jan Jakubův, Karel Chvalovský, Zarathustra Goertzel +6
As a present to Mizar on its 50th anniversary, we develop an AI/TP system that automatically proves about 60\% of the Mizar theorems in the hammer setting. We also automatically pr…
ENIGMA: Efficient Learning-based Inference Guiding Machine
Jan Jakubův, Josef Urban
ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many proof searches are classified as positive and negative b…
BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Jan Jakubuv, Josef Urban
Inventing targeted proof search strategies for specific problem sets is a difficult task. State-of-the-art automated theorem provers (ATPs) such as E allow a large number of user-s…
Expressiveness of Generic Process Shape Types
Jan Jakubuv, J. B. Wells
Shape types are a general concept of process types which work for many process calculi. We extend the previously published Poly* system of shape types to support name restriction.…