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

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

DeepMath
 Referenced in 7 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...

ATPboost
 Referenced in 2 articles
[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...

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...

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 1748 articles
[sw00161]
 Coq is a formal proof management system. It...

Sostools
 Referenced in 262 articles
[sw00891]
 We are pleased to introduce SOSTOOLS, a free...

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

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

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

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

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

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

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

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

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

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

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