7 citations · 14 across the 14 of their papers we have counts for
16 papers
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…
Improving ENIGMA-Style Clause Selection While Learning From History
Martin Suda
We re-examine the topic of machine-learned clause selection guidance in saturation-based theorem provers. The central idea, recently popularized by the ENIGMA system, is to learn a…
Vampire With a Brain Is a Good ITP Hammer
Martin Suda
Vampire has been for a long time the strongest first-order automatic theorem prover, widely used for hammer-style proof automation in ITPs such as Mizar, Isabelle, HOL, and Coq. In…
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
Jan Jakubův, Karel Chvalovský, Miroslav Olšák +3
We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems…
Layered Clause Selection for Theory Reasoning
Bernhard Gleiss, Martin Suda
Explicit theory axioms are added by a saturation-based theorem prover as one of the techniques for supporting theory reasoning. While simple and effective, adding theory axioms can…
Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Martin Suda, Sarah Winkler
These are the post-proceedings of the second ARCADE workshop, which took place on the 26th August 2019 in Natal, Brazil, colocated with CADE-27. ARCADE stands for Automated Reasoni…