3 citations · 6 across the 6 of their papers we have counts for
Showing 2021Show all
2 papers · 1 filter
cs.AI2021
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…
cs.AI2021
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…