21 citations · 21 across the 1 of their papers we have counts for
9 papers
Learning Theorem Proving Components
Karel Chvalovský, Jan Jakubův, Miroslav Olšák +1
Saturation-style automated theorem provers (ATPs) based on the given clause procedure are today the strongest general reasoners for classical first-order logic. The clause selectio…
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…
First Neural Conjecturing Datasets and Experiments
Josef Urban, Jan Jakubův
We describe several datasets and first experiments with creating conjectures by neural methods. The datasets are based on the Mizar Mathematical Library processed in several forms…
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…
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…
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…