21 citations · 29 across the 9 of their papers we have counts for
Showing 2019Show all
3 papers · 1 filter
cs.AI2019
ENIGMAWatch: ProofWatch Meets ENIGMA
Zarathustra Goertzel, Jan Jakubův, Josef Urban
In this work we describe a new learning-based proof guidance -- ENIGMAWatch -- for saturation-style first-order theorem provers. ENIGMAWatch combines two guiding approaches for the…
cs.AI2019★ 21 cited
Hammering Mizar by Learning Clause Guidance
Jan Jakubův, Josef Urban
We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated…
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…