31 citations · 111 across the 8 of their papers we have counts for
17 papers · 1 filter
The Isabelle ENIGMA
Zarathustra A. Goertzel, Jan Jakubův, Cezary Kaliszyk +3
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In parti…
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…
The Role of Entropy in Guiding a Connection Prover
Zsolt Zombori, Josef Urban, Miroslav Olšák
In this work we study how to learn good algorithms for selecting reasoning steps in theorem proving. We explore this in the connection tableau calculus implemented by leanCoP where…
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
We present Tactician, a tactic learner and prover for the Coq Proof Assistant. Tactician helps users make tactical proof decisions while they retain control over the general proof…
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…
Tactic Learning and Proving for the Coq Proof Assistant
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
We present a system that utilizes machine learning for tactic proof search in the Coq Proof Assistant. In a similar vein as the TacticToe project for HOL4, our system predicts appr…