Fetching the paper…
Reading the bibliography…
We describe several additions to the ENIGMA system that guides clause selection in the E automated theorem prover.
A new class of automated theorem-proving algorithms
Ross A. Overbeek · 1974
Earlier work this paper cites.
Bandit processes and dynamic allocation indices
John C Gittins · 1979
Earlier work this paper cites.
The path-indexing method for indexing terms
Mark E Stickel · 1989
Earlier work this paper cites.
Experiments with discrimination-tree indexing and path indexing for term retrieval
William McCune · 1992
Earlier work this paper cites.
The anatomy of Vampire implementing bottom-up procedures with code trees
Andrei Voronkov · 1995
Earlier work this paper cites.
Using hints to increase the effectiveness of an automated reasoning program: Case studies
Robert Veroff · 1996
Earlier work this paper cites.
Citius altius fortius: Lessons learned from the theorem prover WALDMEISTER
Thomas Hillenbrand · 2003
Earlier work this paper cites.
The state of CASC
Geoff Sutcliffe and Christian B. Suttner · 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.
randocop: Randomizing the proof search order in the connection calculus
Thomas Raths and Jens Otten · 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.
Fingerprint indexing for paramodulation and rewriting
Stephan Schulz · 2012
Cited alongside, same era.
Loops with abelian inner mapping groups: An application of automated deduction
Michael K. Kinyon, Robert Veroff, and Petr Vojtechovský · 2013
Cited alongside, same era.
First-order theorem proving and Vampire
Laura Kovács and Andrei Voronkov · 2013
Cited alongside, same era.
System description: E 1.8
Stephan Schulz · 2013
Cited alongside, same era.
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.
Efficient low-level connection tableaux
Cezary Kaliszyk · 2015
Cited alongside, same era.
Deep network guided proof search
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk · 2017
Later among the works it cites.
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.
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.
ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E
Karel Chvalovský, Jan Jakubův, Martin Suda, and Josef Urban · 2019
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
MizAR 40 for Mizar 40
Cezary Kaliszyk and Josef Urban · 2015
Cited alongside, same era.
Tensorflow: Large-scale machine learning on heterogeneous distributed systems
Martın Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Chen Zhifeng, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin Sanjay Ghemawat, Andrew Harp Ian Goodfellow, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Manjunath Kudlur Lukasz Kaiser, Josh Levenberg, Dan Mane, Rajat Monga, Sherry Moore, Derek Murray, Chris Olah, Mike Schuster, Jonathon Shlens, Benoit Steiner, Ilya Sutskever, Paul Tucker Kunal Talwar, Vincent Vanhoucke, Vijay Vasudevan, Fernanda Viegas, Oriol Vinyals, Pete Warden, Martin Wattenberg, Martin Wicke, Yuan Yu, , and Xiaoqiang Zheng · 2016
Cited alongside, same era.
XGBoost: A scalable tree boosting system
Tianqi Chen and Carlos Guestrin · 2016
Cited alongside, same era.
The CADE-25 automated theorem proving system competition - CASC-25
Geoff Sutcliffe and Josef Urban · 2016
Cited alongside, same era.
ENIGMA: efficient learning-based inference guiding machine
Jan Jakubův and Josef Urban · 2017
Cited alongside, same era.
Lightgbm: A highly efficient gradient boosting decision tree
Guolin Ke, Qi Meng, Thomas Finley, Taifeng Wang, Wei Chen, Weidong Ma, Qiwei Ye, and Tie-Yan Liu · 2017
Cited alongside, same era.
Enigmawatch: Proofwatch meets ENIGMA
Zarathustra Goertzel, Jan Jakubův, and Josef Urban · 2019
Later among the works it cites.
Hammering Mizar by learning clause guidance
Jan Jakubův and Josef Urban · 2019
Later among the works it cites.
Faster, higher, stronger: E 2.3
Stephan Schulz, Simon Cruanes, and Petar Vukmirovic · 2019
Later among the works it cites.
ENIGMA anonymous: Symbol-independent inference guiding machine (system description)
Jan Jakubův, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, and Josef Urban · 2020
Later among the works it cites.
Property invariant embedding for automated reasoning
Miroslav Olsák, Cezary Kaliszyk, and Josef Urban · 2020
Later among the works it cites.
Efficient implementation of large-scale watchlists
Constantin Ruhdorfer and Stephan Schulz · 2020
Later among the works it cites.