Fetching the paper…
Reading the bibliography…
Machine Learner for Automated Reasoning (MaLARea) is a learning and reasoning system for proving in large formal libraries where thousands of theorems are available when attacking a new conjecture, and a large number of related problems and proofs can be used to learn specific theorem-proving knowledge.
Étude comparative de la distribution florale dans une portion des Alpes et des Jura
P. Jaccard · 1901
Earlier work this paper cites.
Bandit processes and dynamic allocation indices
J. C. Gittins · 1979
Earlier work this paper cites.
Reinforcement learning: An introduction
R. S. Sutton and A. G. Barto · 1998
Earlier work this paper cites.
The SNoW Learning Architecture
A. Carlson, C. Cumby, J. Rosen, and D. Roth · 1999
Earlier work this paper cites.
E - A Brainiac Theorem Prover
S. Schulz · 2002
Earlier work this paper cites.
Kernel Methods for Pattern Analysis
J. Shawe-Taylor and N. Cristianini · 2004
Earlier work this paper cites.
MPTP - Motivation, Implementation, First Experiments
J. Urban · 2004
Earlier work this paper cites.
MPTP 0.2: Design, implementation, and initial experiments
J. Urban · 2006
Cited alongside, same era.
MaLARea: a metasystem for automated reasoning in large theories
J. Urban · 2007
Cited alongside, same era.
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskočil · 2008
Cited alongside, same era.
SPASS Version 3.5
C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda, and P. Wischnewski · 2009
Cited alongside, same era.
Sine qua non for large theory reasoning
K. Hoder and A. Voronkov · 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.
Stronger automation for Flyspeck by feature weighting and strategy evolution
C. Kaliszyk and J. Urban · 2013
Later among the works it cites.
Learning from multiple proofs: First experiments
D. Kuehlwein and J. Urban · 2013
Later among the works it cites.
MaSh: Machine learning for Sledgehammer
D. Kühlwein, J. C. Blanchette, C. Kaliszyk, and J. Urban · 2013
Later among the works it cites.
ATP and presentation service for Mizar formalizations
J. Urban, P. Rudnicki, and G. Sutcliffe · 2013
Later among the works it cites.
Premise selection for mathematics by corpus analysis and kernel methods
J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban · 2014
Closest in time.
Learning-assisted automated reasoning with Flyspeck
C. Kaliszyk and J. Urban · 2014
Closest in time.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
C. Kaliszyk and J. Urban · 2013
Cited alongside, same era.
J. Urban · 2014
Closest in time.