• MPTP 0.2

  • Referenced in 42 articles [sw02589]
  • fully autonomous mode, in which the premises are selected by a machine-learning 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 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...
  • 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 multi-label ... that estimates the pairwise-relevance 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...
  • UCI-ml

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