BliStr: The Blind Strategymaker

E - A Brainiac Theorem Prover

Stephan Schulz · 2002

Earlier work this paper cites.

MPTP - Motivation, Implementation, First Experiments

Josef Urban · 2004

Earlier work this paper cites.

MoMM - fast interreduction and retrieval in large libraries of formalized mathematics

Josef Urban · 2006

Earlier work this paper cites.

MPTP 0.2: Design, implementation, and initial experiments

Josef Urban · 2006

Earlier work this paper cites.

MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance

Original

Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiří Vyskočil · 2008

Earlier work this paper cites.

ParamILS: an automatic algorithm configuration framework

Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown, and Thomas Stützle · 2009

Cited alongside, same era.

Mizar in a nutshell

Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz · 2010

Cited alongside, same era.

The TPTP world - infrastructure for automated reasoning

Geoff Sutcliffe · 2010

Cited alongside, same era.

Evaluation of automated theorem proving on the Mizar Mathematical Library

Josef Urban, Krystof Hoder, and Andrei Voronkov · 2010

Cited alongside, same era.

Sine qua non for large theory reasoning

Krystof Hoder and Andrei Voronkov · 2011

Cited alongside, same era.

First-order theorem proving and Vampire

Laura Kovács and Andrei Voronkov · 2013

Closest in time.

E-MaLeS 1.1

Daniel Kühlwein, Stephan Schulz, and Josef Urban · 2013

Closest in time.

Premise selection for mathematics by corpus analysis and kernel methods

Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban · 2014

Closest in time.

Learning-assisted automated reasoning with Flyspeck

Cezary Kaliszyk and Josef Urban · 2014

Closest in time.

Machine learner for automated reasoning 0.4 and 0.5

Original

Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil · 2014

Closest in time.