• HOL

  • Referenced in 436 articles [sw05492]
  • Built-in decision procedures and theorem provers can automatically establish many simple theorems. An Oracle...
  • VAMPIRE

  • Referenced in 203 articles [sw02918]
  • Vampire 8.0, [RV02,Vor05] is an automatic theorem prover for first-order classical logic...
  • Sledgehammer

  • Referenced in 101 articles [sw07047]
  • tool that harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations...
  • Pesca

  • Referenced in 92 articles [sw13664]
  • proof editor and as an automatic theorem prover. Proofs constructed in Pesca can both...
  • cvc3

  • Referenced in 84 articles [sw04886]
  • CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. CVC3...
  • CVC4

  • Referenced in 79 articles [sw09485]
  • CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems...
  • Metis_

  • Referenced in 49 articles [sw04439]
  • Metis is an automatic theorem prover for first order logic with equality Features of Metis...
  • Analytica

  • Referenced in 30 articles [sw10478]
  • prover for Mathematica. Analytica is an automatic theorem prover for theorems in elementary analysis ... prover is written in Mathematica language and runs in the Mathematica environment. The goal ... beyond the scope of previous automatic theorem provers. The theorem prover is also able...
  • SPIKE

  • Referenced in 21 articles [sw10186]
  • SPIKE, an automatic theorem prover...
  • GeoThms

  • Referenced in 22 articles [sw06216]
  • that integrates dynamic geometry software (DGS), automatic theorem provers (ATP), and a repository of geometrical...
  • TVOC

  • Referenced in 19 articles [sw02521]
  • Verification conditions are validated using the automatic theorem prover CVC Lite...
  • CeTA

  • Referenced in 39 articles [sw06584]
  • termination proofs using CeTA. There are many automatic tools to prove termination of term rewrite ... this paper we use the theorem prover Isabelle/HOL to automatically certify termination proofs. To this...
  • MaSh

  • Referenced in 17 articles [sw08206]
  • Machine Learning for Sledgehammer. Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL...
  • Zapato

  • Referenced in 11 articles [sw25425]
  • process is applied to software, an automatic theorem prover for quantifier-free first-order logic ... report on a fast, lightweight, and automatic theorem prover called Zapato which we have built...
  • MetiTarski

  • Referenced in 42 articles [sw00573]
  • proved automatically by MetiTarski: a resolution theorem prover (Metis) modified to call a decision procedure...
  • Alt-Ergo

  • Referenced in 13 articles [sw04888]
  • Ergo is an automatic theorem prover dedicated to program verification. Alt-Ergo is based...
  • Cogent

  • Referenced in 13 articles [sw01300]
  • Slam and ESC/Java rely on automatic theorem provers. The existing theorem provers, such as Simplify...
  • ARA

  • Referenced in 5 articles [sw08504]
  • System description: ARA -- an automatic theorem prover for relation algebras. ARA is an automatic theorem...
  • E-MaLeS

  • Referenced in 7 articles [sw15190]
  • important for the success of automatic theorem provers. E-MaLeS is a meta-system that...