• HOL

  • Referenced in 557 articles [sw05492]
  • proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish...
  • CLAM

  • Referenced in 40 articles [sw19619]
  • interactive proof editor into a fully automatic theorem proving system...
  • IsaPlanner

  • Referenced in 30 articles [sw02047]
  • used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that...
  • ETPS

  • Referenced in 158 articles [sw06302]
  • used to prove theorems of first- and higher-order logic interactively, automatically...
  • Epsilon

  • Referenced in 41 articles [sw00244]
  • inequations, and handle and prove geometric theorems automatically...
  • ML

  • Referenced in 517 articles [sw01218]
  • polymorphic Hindley–Milner type system, which automatically assigns the types of most expressions without requiring ... such as in compiler writing, automated theorem proving and formal verification. (wikipedia...
  • Walnut

  • Referenced in 24 articles [sw30122]
  • Automatic Theorem Proving in Walnut. Walnut is a software package that implements a mechanical decision ... some special words referred to as automatic words or automatic sequences. Walnut is written...
  • VAMPIRE

  • Referenced in 241 articles [sw02918]
  • Vampire 8.0, [RV02,Vor05] is an automatic theorem prover for first-order classical logic ... result to the kernel. When a theorem is proved, the system produces a verifiable proof...
  • MetiTarski

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

  • Referenced in 111 articles [sw09485]
  • automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove...
  • TPS

  • Referenced in 71 articles [sw00973]
  • used to prove theorems of first- and higher-order logic interactively, automatically...
  • HipSpec

  • Referenced in 14 articles [sw07736]
  • HipSpec is a system for automatically deriving and proving properties about functional programs. It uses ... exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems ... used as a background theory for proving additional user-stated properties. Experimental results are encouraging...
  • Zapato

  • Referenced in 11 articles [sw25425]
  • zapato: Automatic theorem proving for predicate abstraction refinement. Counterexample-driven abstraction refinement is an automatic ... process is applied to software, an automatic theorem prover for quantifier-free first-order logic...
  • MUSCADET

  • Referenced in 10 articles [sw06859]
  • MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics. The author presents ... knowledge base is adapted to prove theorems in point-set topology and topological linear spaces ... main ideas are exemplified by automatic proofs of some elementary facts on topological linear spaces...
  • Electronic Geometry Textbook

  • Referenced in 8 articles [sw08745]
  • resulting textbook. By integrating an external geometric theorem prover and an external dynamic geometry software ... system offers the facilities for automatically proving theorems and generating dynamic figures in the created...
  • SymbolicData

  • Referenced in 28 articles [sw04621]
  • benchmarking of different geometry theorem proving approaches and provers. To automatize such tests...
  • PARTHENON

  • Referenced in 8 articles [sw25434]
  • role of parallelism in automatic theorem proving for future research...
  • GEOTHER 1.1

  • Referenced in 31 articles [sw02842]
  • manipulate and prove the theorem. From the specification, GEOTHER can automatically assign coordinates to each ... manner; translate the predicate representation of the theorem into an English or Chinese statement, into ... draw one or several diagrams for the theorem - the drawn diagrams may be animated ... dragging, and saved as PostScript files; prove the theorem using any of the five algebraic...
  • jStar

  • Referenced in 32 articles [sw11261]
  • automatic verification system, called jStar, which combines theorem proving and abstract interpretation techniques. We demonstrate...
  • Tac

  • Referenced in 7 articles [sw09455]
  • Focused inductive theorem proving. Focused proof systems provide means for reducing and structuring ... capable of automatically proving many theorems using induction and coinduction. Since the automatic proof procedure ... with several examples of proved theorems, some achieved entirely automatically and others achieved with user...