Fetching the paper…
Reading the bibliography…
Automated reasoning and theorem proving have recently become major challenges for machine learning.
Ross A. Overbeek, ‘A new class of automated theorem-proving algorithms’, J. ACM
1974
Earlier work this paper cites.
Wolfgang Ertel, Johann Schumann, and Christian B. Suttner, ‘Learning heuristics for a theorem prover using back propagation’, in 5. Österreichische Artificial Intelligence-Tagung, Igls, Tirol, 28. bis 30. September 1989, Proceedings
1989
Earlier work this paper cites.
Reinhold Letz, Klaus Mayr, and Christoph Goller, ‘Controlled integration of the cut rule into connection tableau calculi’, Journal of Automated Reasoning
1994
Earlier work this paper cites.
Christoph Goller and Andreas Küchler, ‘Learning task-dependent distributed representations by backpropagation through structure’, in Proceedings of International Conference on Neural Networks (ICNN’96), Washington, DC, USA, June 3-6, 1996
1996
Earlier work this paper cites.
Jörg Denzinger, Matthias Fuchs, Christoph Goller, and Stephan Schulz, ‘Learning from Previous Proof Experience’, Technical Report AR99-4, Institut für Informatik, Technische Universität München, (1999)
1999
Earlier work this paper cites.
Stephan Schulz, Learning search control knowledge for equational deduction
2000
Earlier work this paper cites.
Handbook of Automated Reasoning (in 2 volumes)
2001
Earlier work this paper cites.
Jens Otten and Wolfgang Bibel, ‘leanCoP: lean connection-based theorem proving’, J. Symb. Comput
2003
Earlier work this paper cites.
Josef Urban, ‘MPTP - Motivation, Implementation, First Experiments’, J. Autom. Reasoning
2004
Earlier work this paper cites.
Josef Urban, ‘MPTP 0.2: Design, implementation, and initial experiments’, J. Autom. Reasoning
2006
Earlier work this paper cites.
Jia Meng and Lawrence C. Paulson, ‘Translating higher-order clauses to first-order clauses’, J. Autom. Reasoning
2008
Earlier work this paper cites.
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiří Vyskočil, ‘MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance’, in IJCAR
2008
Earlier work this paper cites.
Jens Otten, ‘Restricting backtracking in connection calculi’, AI Commun
2010
Earlier work this paper cites.
Geoff Sutcliffe, ‘The TPTP world - infrastructure for automated reasoning’, in LPAR (Dakar)
2010
Earlier work this paper cites.
Josef Urban, Jiří Vyskočil, and Petr Štěpánek, ‘MaLeCoP: Machine learning connection prover’, in TABLEAUX
2011
Earlier work this paper cites.
Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes, ‘Overview and evaluation of premise selection techniques for large theory mathematics’, in IJCAR
2012
Cited alongside, same era.
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban, ‘Premise selection for mathematics by corpus analysis and kernel methods’, J. Autom. Reasoning
2014
Cited alongside, same era.
Cezary Kaliszyk and Josef Urban, ‘Learning-assisted automated reasoning with Flyspeck’, J. Autom. Reasoning
2014
Cited alongside, same era.
Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings
Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, eds · 2015
Cited alongside, same era.
Michael Färber, Cezary Kaliszyk, and Josef Urban, ‘Monte Carlo tableau proof search’, in Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings
2017
Later among the works it cites.
Jan Jakubuv and Josef Urban, ‘ENIGMA: efficient learning-based inference guiding machine’, in Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings
2017
Later among the works it cites.
Cezary Kaliszyk, François Chollet, and Christian Szegedy, ‘HolStep: A machine learning dataset for higher-order logic theorem proving’, in 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings
2017
Later among the works it cites.
Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk, ‘Deep network guided proof search’, in LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
David Duvenaud, Dougal Maclaurin, Jorge Aguilera-Iparraguirre, Rafael Gómez-Bombarelli, Timothy Hirzel, Alán Aspuru-Guzik, and Ryan P. Adams, ‘Convolutional networks on graphs for learning molecular fingerprints’, in Advances in Neural Information Processing Systems 28: Annual Conference on Neural Information Processing Systems 2015, December 7-12, 2015, Montreal, Quebec, Canada
2015
Cited alongside, same era.
http://dx.doi.org/10.1145/2676724.2693173
Thibault Gauthier and Cezary Kaliszyk, ‘Premise selection and external provers for HOL4’, in Certified Programs and Proofs (CPP’15) · 2015
Cited alongside, same era.
Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015
Georg Gottlob, Geoff Sutcliffe, and Andrei Voronkov, eds · 2015
Cited alongside, same era.
Cezary Kaliszyk and Josef Urban, ‘HOL(y)Hammer: Online ATP service for HOL Light’, Mathematics in Computer Science
2015
Cited alongside, same era.
Cezary Kaliszyk and Josef Urban, ‘MizAR 40 for Mizar 40’, J. Autom. Reasoning
2015
Cited alongside, same era.
Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil, ‘Efficient semantic features for automated reasoning over large theories’, in IJCAI
2015
Cited alongside, same era.
Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban, ‘DeepMath - deep sequence models for premise selection’, in Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain
2016
Cited alongside, same era.
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban, ‘A learning-based fact selector for Isabelle/HOL’, J. Autom. Reasoning
2016
Cited alongside, same era.
2017
Later among the works it cites.
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk, ‘Deep network guided proof search’, in LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017
2017
Later among the works it cites.
David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al., ‘Mastering the game of go without human knowledge’, Nature
2017
Later among the works it cites.
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng, ‘Premise selection for theorem proving by deep graph embedding’, in Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, 4-9 December 2017, Long Beach, CA, USA
2017
Later among the works it cites.
Jan Jakubův and Josef Urban, ‘Hierarchical invention of theorem proving strategies’, AI Commun
2018
Later among the works it cites.
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák, ‘Reinforcement learning of theorem proving’, in Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December 2018, Montréal, Canada
2018
Later among the works it cites.
Kriste Krstovski and David M. Blei, ‘Equation embeddings’, CoRR
2018
Later among the works it cites.
2018
Later among the works it cites.
Karel Chvalovský, Jan Jakubuv, Martin Suda, and Josef Urban, ‘ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E’, in Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings
2019
Closest in time.
Thibault Gauthier and Cezary Kaliszyk, ‘Aligning concepts across proof assistant libraries’, J. Symb. Comput
2019
Closest in time.
Jan Jakubuv and Josef Urban, ‘Hammering Mizar by learning clause guidance’, in 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA
2019
Closest in time.
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill, ‘Learning a SAT solver from single-bit supervision’, in 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019
2019
Closest in time.