Fetching the paper…
Reading the bibliography…
We describe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach.
Otter 2.0
William McCune · 1990
Earlier work this paper cites.
Long short-term memory
Sepp Hochreiter and Jürgen Schmidhuber · 1997
Earlier work this paper cites.
Handbook of Automated Reasoning (in 2 volumes)
John Alan Robinson and Andrei Voronkov, editors · 2001
Earlier work this paper cites.
E - A Brainiac Theorem Prover
Stephan Schulz · 2002
Earlier work this paper cites.
leanCoP: lean connection-based theorem proving
Jens Otten and Wolfgang Bibel · 2003
Earlier work this paper cites.
Ensemble based systems in decision making
Robi Polikar · 2006
Earlier work this paper cites.
MPTP 0.2: Design, implementation, and initial experiments
Josef Urban · 2006
Earlier work this paper cites.
LIBLINEAR: A library for large linear classification
Rong-En Fan, Kai-Wei Chang, Cho-Jui Hsieh, Xiang-Rui Wang, and Chih-Jen Lin · 2008
Earlier work this paper cites.
Translating higher-order clauses to first-order clauses
Jia Meng and Lawrence C. Paulson · 2008
Earlier work this paper cites.
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiří Vyskočil · 2008
Earlier work this paper cites.
MaLeCoP: Machine learning connection prover
Josef Urban, Jiří Vyskočil, and Petr Štěpánek · 2011
Earlier work this paper cites.
Overview and evaluation of premise selection techniques for large theory mathematics
Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes · 2012
Earlier work this paper cites.
Semantic compositionality through recursive matrix-vector spaces
Richard Socher, Brody Huval, Christopher D. Manning, and Andrew Y. Ng · 2012
Earlier work this paper cites.
First-order theorem proving and Vampire
Laura Kovács and Andrei Voronkov · 2013
Cited alongside, same era.
Learning from multiple proofs: First experiments
Daniel Kuehlwein and Josef Urban · 2013
Cited alongside, same era.
Premise selection for mathematics by corpus analysis and kernel methods
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban · 2014
Cited alongside, same era.
Learning-assisted automated reasoning with Flyspeck
Cezary Kaliszyk and Josef Urban · 2014
Cited alongside, same era.
Mizar: State-of-the-art and beyond
Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban · 2015
Cited alongside, same era.
Premise selection and external provers for HOL4
Thibault Gauthier and Cezary Kaliszyk · 2015
Cited alongside, same era.
Performance of clause selection heuristics for saturation-based theorem proving
Stephan Schulz and Martin Möhrmann · 2016
Later among the works it cites.
Monte Carlo tableau proof search
Michael Färber, Cezary Kaliszyk, and Josef Urban · 2017
Later among the works it cites.
ENIGMA: efficient learning-based inference guiding machine
Jan Jakubův and Josef Urban · 2017
Later among the works it cites.
BliStrTune: hierarchical invention of theorem proving strategies
Jan Jakubuv and Josef Urban · 2017
Later among the works it cites.
Bag of tricks for efficient text classification
Armand Joulin, Edouard Grave, Piotr Bojanowski, and Tomas Mikolov · 2017
Later among the works it cites.
Deep network guided proof search
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk · 2017
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015
Georg Gottlob, Geoff Sutcliffe, and Andrei Voronkov, editors · 2015
Cited alongside, same era.
FEMaLeCoP: Fairly efficient machine learning connection prover
Cezary Kaliszyk and Josef Urban · 2015
Cited alongside, same era.
Efficient semantic features for automated reasoning over large theories
Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil · 2015
Cited alongside, same era.
DeepMath - deep sequence models for premise selection
Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban · 2016
Cited alongside, same era.
A learning-based fact selector for Isabelle/HOL
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban · 2016
Cited alongside, same era.
Hammering towards QED
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban · 2016
Cited alongside, same era.
ProofWatch: Watchlist guidance for large theories in E
Zarathustra Goertzel, Jan Jakubův, Stephan Schulz, and Josef Urban · 2018
Later among the works it cites.
ProofWatch meets ENIGMA: First experiments
Zarathustra Goertzel, Jan Jakubuv, and Josef Urban · 2018
Later among the works it cites.
Enhancing ENIGMA given clause guidance
Jan Jakubův and Josef Urban · 2018
Later among the works it cites.
Hierarchical invention of theorem proving strategies
Jan Jakubův and Josef Urban · 2018
Later among the works it cites.
Reinforcement learning of theorem proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olsák · 2018
Later among the works it cites.
ATPboost: Learning premise selection in binary setting with ATP feedback
Bartosz Piotrowski and Josef Urban · 2018
Later among the works it cites.