ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback

E - A Brainiac Theorem Prover

S. Schulz · 2002

Earlier work this paper cites.

MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance

J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskočil · 2008

Earlier work this paper cites.

The TPTP problem library and associated infrastructure

G. Sutcliffe · 2009

Earlier work this paper cites.

MaLeCoP: Machine learning connection prover

J. Urban, J. Vyskočil, and P. Štěpánek · 2011

Earlier work this paper cites.

Learning from multiple proofs: First experiments

D. Kuehlwein and J. Urban · 2013

Earlier work this paper cites.

Premise selection for mathematics by corpus analysis and kernel methods

J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban · 2014

Cited alongside, same era.

Learning-assisted automated reasoning with Flyspeck

C. Kaliszyk and J. Urban · 2014

Cited alongside, same era.

FEMaLeCoP: Fairly efficient machine learning connection prover

C. Kaliszyk and J. Urban · 2015

Cited alongside, same era.

Mizar 40 for mizar 40

C. Kaliszyk and J. Urban · 2015

Cited alongside, same era.

DeepMath - Deep Sequence Models for Premise Selection

A. A. Alemi, F. Chollet, G. Irving, C. Szegedy, and J. Urban, editors · 2016

Cited alongside, same era.

TacticToe: Learning to reason with HOL4 tactics

T. Gauthier, C. Kaliszyk, and J. Urban

Cited in the paper.

Deep network guided proof search

S. M. Loos, G. Irving, C. Szegedy, and C. Kaliszyk

Cited in the paper.

A learning-based fact selector for Isabelle/HOL

J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban · 2016

Later among the works it cites.

Hammering towards QED

J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban · 2016

Later among the works it cites.

Xgboost: A scalable tree boosting system

T. Chen and C. Guestrin · 2016

Later among the works it cites.

LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017

T. Eiter and D. Sands, editors · 2017

Later among the works it cites.

ENIGMA: efficient learning-based inference guiding machine

J. Jakubuv and J. Urban · 2017

Later among the works it cites.