Fetching the paper…
Reading the bibliography…
We introduce a theorem proving algorithm that uses practically no domain heuristics for guiding its connection-style proof search.
A machine-oriented logic based on the resolution principle
J. A. Robinson · 1965
Earlier work this paper cites.
Otter 2.0
W. McCune · 1990
Earlier work this paper cites.
Rewrite-based equational theorem proving with selection and simplification
L. Bachmair and H. Ganzinger · 1994
Earlier work this paper cites.
Controlled integration of the cut rule into connection tableau calculi
R. Letz, K. Mayr, and C. Goller · 1994
Earlier work this paper cites.
Reinforcement learning: An introduction
R. S. Sutton and A. G. Barto · 1998
Earlier work this paper cites.
Handbook of Automated Reasoning (in 2 volumes)
J. A. Robinson and A. Voronkov, editors · 2001
Earlier work this paper cites.
leanCoP: lean connection-based theorem proving
J. Otten and W. Bibel · 2003
Earlier work this paper cites.
Bandit based monte-carlo planning
L. Kocsis and C. Szepesvári · 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.-E. Fan, K.-W. Chang, C.-J. Hsieh, X.-R. Wang, and C.-J. Lin · 2008
Earlier work this paper cites.
Translating higher-order clauses to first-order clauses
J. Meng and L. C. Paulson · 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.
Satisfiability modulo theories
C. W. Barrett, R. Sebastiani, S. A. Seshia, C. Tinelli, et al · 2009
Earlier work this paper cites.
Mizar in a nutshell
A. Grabowski, A. Korniłowicz, and A. Naumowicz · 2010
Earlier work this paper cites.
Restricting backtracking in connection calculi
J. Otten · 2010
Earlier work this paper cites.
Scikit-learn: Machine learning in Python
F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay · 2011
Cited alongside, same era.
MaLeCoP: Machine learning connection prover
J. Urban, J. Vyskočil, and P. Štěpánek · 2011
Cited alongside, same era.
Overview and evaluation of premise selection techniques for large theory mathematics
D. Kühlwein, T. van Laarhoven, E. Tsivtsivadze, J. Urban, and T. Heskes · 2012
Cited alongside, same era.
Premise selection for mathematics by corpus analysis and kernel methods
J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban · 2014
Cited alongside, same era.
Learning-assisted automated reasoning with Flyspeck
C. Kaliszyk and J. Urban · 2014
Cited alongside, same era.
Machine learner for automated reasoning 0.4 and 0.5
C. Kaliszyk, J. Urban, and J. Vyskočil · 2014
A learning-based fact selector for Isabelle/HOL
J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban · 2016
Later among the works it cites.
Hammering towards QED
J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban · 2016
Later among the works it cites.
XGBoost: A scalable tree boosting system
T. Chen and C. Guestrin · 2016
Later among the works it cites.
Mastering the game of Go with deep neural networks and tree search
D. Silver, A. Huang, C. J. Maddison, A. Guez, L. Sifre, G. van den Driessche, J. Schrittwieser, I. Antonoglou, V. Panneershelvam, M. Lanctot, S. Dieleman, D. Grewe, J. Nham, N. Kalchbrenner, I. Sutskever, T. P. Lillicrap, M. Leach, K. Kavukcuoglu, T. Graepel, and D. Hassabis · 2016
Later among the works it cites.
Holophrasm: a neural automated theorem prover for higher-order logic
D. Whalen · 2016
Later among the works it cites.
Thinking fast and slow with deep learning and tree search
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Premise selection and external provers for HOL4
T. Gauthier 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.
Certified connection tableaux proofs for HOL Light and TPTP
C. Kaliszyk, J. Urban, and J. Vyskočil · 2015
Cited alongside, same era.
Breeding theorem proving heuristics with genetic algorithms
S. Schäfer and S. Schulz · 2015
Cited alongside, same era.
T. Anthony, Z. Tian, and D. Barber · 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.
TacticToe: Learning to reason with HOL4 tactics
T. Gauthier, C. Kaliszyk, and J. Urban · 2017
Later among the works it cites.
BliStrTune: hierarchical invention of theorem proving strategies
J. Jakubuv and J. Urban · 2017
Later among the works it cites.
ENIGMA: efficient learning-based inference guiding machine
J. Jakubuv and J. Urban · 2017
Later among the works it cites.
Deep network guided proof search
S. M. Loos, G. Irving, C. Szegedy, and C. Kaliszyk · 2017
Later among the works it cites.
Mastering chess and shogi by self-play with a general reinforcement learning algorithm
D. Silver, T. Hubert, J. Schrittwieser, I. Antonoglou, M. Lai, A. Guez, M. Lanctot, L. Sifre, D. Kumaran, T. Graepel, T. P. Lillicrap, K. Simonyan, and D. Hassabis · 2017
Later among the works it cites.
Mastering the game of go without human knowledge
D. Silver, J. Schrittwieser, K. Simonyan, I. Antonoglou, A. Huang, A. Guez, T. Hubert, L. Baker, M. Lai, A. Bolton, et al · 2017
Later among the works it cites.
ATPboost: Learning premise selection in binary setting with ATP feedback
B. Piotrowski and J. Urban · 2018
Closest in time.