Showing cs.AIShow all
3 papers · 1 filter
cs.AI2021
Fast and Slow Enigmas and Parental Guidance
Zarathustra Goertzel, Karel Chvalovský, Jan Jakubův +2
We describe several additions to the ENIGMA system that guides clause selection in the E automated theorem prover. First, we significantly speed up its neural guidance by adding se…
cs.AI2020
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…
cs.AI2019
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…