Fetching the paper…
Reading the bibliography…
HOL(y)Hammer is an online AI/ATP service for formal (computer-understandable) mathematics encoded in the HOL Light system.
The distance-weighted k-nearest-neighbor rule
Sahibsingh A. Dudani · 1976
Earlier work this paper cites.
A Fire Upon the Deep
Vernor Vinge · 1992
Earlier work this paper cites.
The HOL logic
Andrew Pitts · 1993
Earlier work this paper cites.
HOL Light: A tutorial introduction
John Harrison · 1996
Earlier work this paper cites.
Optimizing Proof Search in Model Elimination
John Harrison · 1996
Earlier work this paper cites.
The SNoW Learning Architecture
Andy Carlson, Chad Cumby, Jeff Rosen, and Dan Roth · 1999
Earlier work this paper cites.
The design and implementation of VAMPIRE
Alexandre Riazanov and Andrei Voronkov · 2002
Earlier work this paper cites.
E - A Brainiac Theorem Prover
Stephan Schulz · 2002
Earlier work this paper cites.
Introduction to the Flyspeck project
Thomas C. Hales · 2005
Earlier work this paper cites.
Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings
Ulrich Furbach and Natarajan Shankar, editors · 2006
Earlier work this paper cites.
MoMM - fast interreduction and retrieval in large libraries of formalized mathematics
Josef Urban · 2006
Earlier work this paper cites.
Source-level proof reconstruction for interactive theorem proving
Lawrence C. Paulson and Kong Woei Susanto · 2007
Earlier work this paper cites.
Z3: An Efficient SMT Solver
Leonardo Mendonça de Moura and Nikolaj Bjørner · 2008
Cited alongside, same era.
Translating higher-order clauses to first-order clauses
Jia Meng and Lawrence C. Paulson · 2008
Cited alongside, same era.
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiří Vyskočil · 2008
Cited alongside, same era.
MetiTarski: An automatic theorem prover for real-valued special functions
Behzad Akbarpour and Lawrence C. Paulson · 2010
Cited alongside, same era.
Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers
Lawrence C. Paulson and Jasmin Blanchette · 2010
Cited alongside, same era.
Automated reasoning and presentation support for formalizing mathematics in Mizar
Josef Urban and Geoff Sutcliffe · 2010
WorkingWiki: a MediaWiki-based platform for collaborative research
Lee Worden · 2011
Later among the works it cites.
Learning-assisted automated reasoning with Flyspeck
Cezary Kaliszyk and Josef Urban · 2012
Later among the works it 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
Later among the works it cites.
Josef Urban · 2012
Later among the works it cites.
Encoding Monomorphic and Polymorphic Types
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone · 2013
Closest in time.
Scalable LCF-style proof translation
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Cited alongside, same era.
Large formal wikis: Issues and solutions
Jesse Alama, Kasper Brink, Lionel Mamane, and Josef Urban · 2011
Cited alongside, same era.
Sine qua non for large theory reasoning
Krystof Hoder and Andrei Voronkov · 2011
Cited alongside, same era.
An Overview of Methods for Large-Theory Automated Theorem Proving (Invited Paper)
Josef Urban · 2011
Cited alongside, same era.
Content-based encoding of mathematical and code libraries
Josef Urban · 2011
Cited alongside, same era.
MaLeCoP: Machine learning connection prover
Josef Urban, Jiří Vyskočil, and Petr Štěpánek · 2011
Cited alongside, same era.
TFF1: The TPTP typed first-order form with rank-1 polymorphism
Jasmin Christian Blanchette and Andrei Paskevich
Cited in the paper.
Cezary Kaliszyk and Alexander Krauss · 2013
Closest in time.
PRocH: Proof reconstruction for HOL Light
Cezary Kaliszyk and Josef Urban · 2013
Closest in time.
Stronger automation for Flyspeck by feature weighting and strategy evolution
Cezary Kaliszyk and Josef Urban · 2013
Closest in time.
Formal mathematics on display: A wiki for Flyspeck
Carst Tankink, Cezary Kaliszyk, Josef Urban, and Herman Geuvers · 2013
Closest in time.
BliStr: The Blind Strategymaker
Josef Urban · 2013
Closest in time.
ATP and presentation service for Mizar formalizations
Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe · 2013
Closest in time.