Fetching the paper…
Reading the bibliography…
We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving.
E - A Brainiac Theorem Prover
S. Schulz · 2002
Earlier work this paper cites.
Ensemble based systems in decision making
R. Polikar · 2006
Earlier work this paper cites.
MPTP 0.2: Design, implementation, and initial experiments
J. Urban · 2006
Earlier work this paper cites.
LIBLINEAR: A library for large linear classification
R. Fan, K. Chang, C. Hsieh, X. Wang, and C. Lin · 2008
Earlier work this paper cites.
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskočil · 2008
Earlier work this paper cites.
Mizar in a nutshell
A. Grabowski, A. Korniłowicz, and A. Naumowicz · 2010
Earlier work this paper cites.
MaLeCoP: Machine learning connection prover
J. Urban, J. Vyskočil, and P. Štěpánek · 2011
Earlier work this paper cites.
First-order theorem proving and Vampire
L. Kovács and A. Voronkov · 2013
Earlier work this paper cites.
System description: E 1.8
S. Schulz · 2013
Earlier work this paper cites.
Premise selection for mathematics by corpus analysis and kernel methods
J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban · 2014
Earlier work this paper cites.
Learning-assisted automated reasoning with Flyspeck
C. Kaliszyk and J. Urban · 2014
Cited alongside, same era.
Random forests for premise selection
M. Färber and C. Kaliszyk · 2015
Cited alongside, same era.
SEPIA: search for proofs using inferred automata
T. Gransden, N. Walkinshaw, and R. Raman · 2015
Cited alongside, same era.
FEMaLeCoP: Fairly efficient machine learning connection prover
C. Kaliszyk and J. Urban · 2015
Cited alongside, same era.
MizAR 40 for Mizar 40
C. Kaliszyk and J. Urban · 2015
Cited alongside, same era.
Efficient semantic features for automated reasoning over large theories
C. Kaliszyk, J. Urban, and J. Vyskocil · 2015
Cited alongside, same era.
LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017
T. Eiter and D. Sands, editors · 2017
Later among the works it cites.
Monte Carlo tableau proof search
M. Färber, C. Kaliszyk, and J. Urban · 2017
Later among the works it cites.
BliStrTune: hierarchical invention of theorem proving strategies
J. Jakubův and J. Urban · 2017
Later among the works it cites.
ENIGMA: efficient learning-based inference guiding machine
J. Jakubův and J. Urban · 2017
Later among the works it cites.
ProofWatch: Watchlist guidance for large theories in E
Z. Goertzel, J. Jakubův, S. Schulz, and J. Urban · 2018
Later among the works it cites.
ProofWatch meets ENIGMA: First experiments
Z. Goertzel, J. Jakubuv, and J. Urban · 2018
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
A. A. Alemi, F. Chollet, N. Eén, G. Irving, C. Szegedy, and J. Urban · 2016
Cited alongside, same era.
A learning-based fact selector for Isabelle/HOL
J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban · 2016
Cited alongside, same era.
Hammering towards QED
J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban · 2016
Cited alongside, same era.
Xgboost: A scalable tree boosting system
T. Chen and C. Guestrin · 2016
Cited alongside, same era.
TacticToe: Learning to reason with HOL4 tactics
T. Gauthier, C. Kaliszyk, and J. Urban
Cited in the paper.
Deep network guided proof search
S. M. Loos, G. Irving, C. Szegedy, and C. Kaliszyk
Cited in the paper.
Enhancing ENIGMA given clause guidance
J. Jakubův and J. Urban · 2018
Later among the works it cites.
Reinforcement learning of theorem proving
C. Kaliszyk, J. Urban, H. Michalewski, and M. Olsák · 2018
Later among the works it cites.
ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E
K. Chvalovský, J. Jakubuv, M. Suda, and J. Urban · 2019
Closest in time.