• MetiTarski

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

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

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

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

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

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

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

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

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

  • Referenced in 18 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 98 articles [sw10277]
  • Communicating formal proofs: the case of flyspeck. We...
  • MaLARea

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

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