149 citations · 825 across the 48 of their papers we have counts for
6 papers · 1 filter
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…
Prolog Technology Reinforcement Learning Prover
Zsolt Zombori, Josef Urban, Chad E. Brown
We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to exte…
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…
Stateful Premise Selection by Recurrent Neural Networks
Bartosz Piotrowski, Josef Urban
In this work, we develop a new learning-based method for selecting facts (premises) when proving new goals over large formal libraries. Unlike previous methods that choose sets of…
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…