• MetiTarski

  • Referenced in 49 articles [sw00573]
  • Many inequalities involving the functions ln, exp, sin...
  • ML

  • Referenced in 498 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • VAMPIRE

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

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

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

  • Referenced in 32 articles [sw04655]
  • MoMM (in the narrower sense) is a tool...
  • Mizar

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

  • Referenced in 465 articles [sw04887]
  • Z3 is a high-performance theorem prover being...
  • HOL

  • Referenced in 472 articles [sw05492]
  • Higher Order Logic (HOL) is a programming environment...
  • MaLeCoP

  • Referenced in 20 articles [sw07197]
  • MaLeCoP Machine Learning Connection Prover. Probabilistic guidance based...
  • PRocH

  • Referenced in 11 articles [sw10191]
  • PRocH: Proof Reconstruction for HOL Light. PRocH is...
  • Flyspeck

  • Referenced in 107 articles [sw10277]
  • Communicating formal proofs: the case of flyspeck. We...
  • MaLARea

  • Referenced in 42 articles [sw10278]
  • MaLARea: a Metasystem for Automated Reasoning in Large...
  • BliStr

  • Referenced in 15 articles [sw16818]
  • BliStr: The Blind Strategymaker. BliStr is a system...