• MPTP 0.2

  • Referenced in 50 articles [sw02589]
  • fully autonomous mode, in which the premises are selected by a machine-learning system trained...
  • HOLyHammer

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

  • Referenced in 11 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 6 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 4 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...
  • NAPSAC

  • Referenced in 3 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 1890 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Sostools

  • Referenced in 289 articles [sw00891]
  • We are pleased to introduce SOSTOOLS, a free...
  • MPTP

  • Referenced in 26 articles [sw02489]
  • We describe a number of new possibilities for...
  • VAMPIRE

  • Referenced in 258 articles [sw02918]
  • Vampire 8.0, [RV02,Vor05] is an automatic theorem...
  • SeDuMi

  • Referenced in 1281 articles [sw04002]
  • SeDuMi is a Matlab toolbox for solving optimization...
  • UCI-ml

  • Referenced in 3403 articles [sw04074]
  • UC Irvine Machine Learning Repository. We currently maintain...
  • gensim

  • Referenced in 15 articles [sw04081]
  • Gensim is a free Python framework designed to...
  • SPASS

  • Referenced in 185 articles [sw04108]
  • SPASS is an automated theorem prover for first...
  • TPTP

  • Referenced in 395 articles [sw04143]
  • The TPTP (Thousands of Problems for Theorem Provers...
  • Metis_

  • Referenced in 56 articles [sw04439]
  • Metis is an automatic theorem prover for first...
  • YALMIP

  • Referenced in 1033 articles [sw04595]
  • YALMIP Yet another LMI parser. YALMIP is a...
  • Mizar

  • Referenced in 505 articles [sw04704]
  • The Mizar System is the only implementation of...
  • LIBSVM

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