
MPTP 0.2
 Referenced in 42 articles
[sw02589]
 fully autonomous mode, in which the premises are selected by a machinelearning system trained...

HOLyHammer
 Referenced in 18 articles
[sw11553]
 automated reasoning systems combined with several premise selection methods trained on all the project proofs...

DeepMath
 Referenced in 6 articles
[sw27551]
 DeepMath  Deep Sequence Models for Premise Selection. We study the effectiveness of neural sequence models ... premise selection in automated theorem proving, one of the main bottlenecks in the formalization ... that yields good results for the premise selection task on the Mizar corpus while avoiding...

TacticToe
 Referenced in 3 articles
[sw28627]
 different tacticlevel proof paths, guiding their selection by learning from a large number ... level. By combining tactic prediction and premise selection, TacticToe is able to reprove...

ATPboost
 Referenced in 1 article
[sw28626]
 ATPboost: learning premise selection in binary setting with ATP feedback. ATPboost is a system ... machine learning of premise selection from the proofs. Unlike many approaches that use multilabel ... that estimates the pairwiserelevance of (theorem, premise) pairs. ATPboost uses for this the fast...

NAPSAC
 Referenced in 4 articles
[sw28051]
 their basis in selecting random minimal sets of data to instantiate hypotheses. However, their perfor ... another than outliers. Based on this premise, the NAPSAC (N Adjacent Points SAmple Consensus) algorithm...

Coq
 Referenced in 1526 articles
[sw00161]
 Coq is a formal proof management system. It...

MPTP
 Referenced in 21 articles
[sw02489]
 We describe a number of new possibilities for...

VAMPIRE
 Referenced in 203 articles
[sw02918]
 Vampire 8.0, [RV02,Vor05] is an automatic theorem...

SeDuMi
 Referenced in 985 articles
[sw04002]
 SeDuMi is a Matlab toolbox for solving optimization...

UCIml
 Referenced in 2617 articles
[sw04074]
 UC Irvine Machine Learning Repository. We currently maintain...

gensim
 Referenced in 9 articles
[sw04081]
 Gensim is a free Python framework designed to...

SPASS
 Referenced in 154 articles
[sw04108]
 SPASS is an automated theorem prover for first...

Metis_
 Referenced in 49 articles
[sw04439]
 Metis is an automatic theorem prover for first...

YALMIP
 Referenced in 744 articles
[sw04595]
 YALMIP Yet another LMI parser. YALMIP is a...

Mizar
 Referenced in 387 articles
[sw04704]
 The Mizar System is the only implementation of...

LIBSVM
 Referenced in 855 articles
[sw04879]
 LIBSVM is a library for Support Vector Machines...

z3
 Referenced in 417 articles
[sw04887]
 Z3 is a highperformance theorem prover being...