2 papers
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…