3 citations · 6 across the 5 of their papers we have counts for
6 papers · 1 filter
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…
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
Karel Chvalovský, Jan Jakubův, Martin Suda +1
We describe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach. Unlike in the first ENIGMA implementation wh…
Selecting the Selection
Giles Reger, Martin Suda, Andrei Voronkov +1
Modern saturation-based Automated Theorem Provers typically implement the superposition calculus for reasoning about first-order logic with or without equality. Practical implement…
Duality in STRIPS planning
Martin Suda
We describe a duality mapping between STRIPS planning tasks. By exchanging the initial and goal conditions, taking their respective complements, and swapping for every action its p…