• MPTP 0.2

  • Referenced in 43 articles [sw02589]
  • fully autonomous mode, in which the premises are selected by a machine-learning 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 multi-label ... that estimates the pairwise-relevance of (theorem, premise) pairs. ATPboost uses for this the fast...
  • TacticToe

  • Referenced in 3 articles [sw28627]
  • different tactic-level proof paths, guiding their selection by learning from a large number ... level. By combining tactic prediction and premise selection, TacticToe is able to re-prove...
  • 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...
  • UCI-ml

  • 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 high-performance theorem prover being...