
HOL
 Referenced in 349 articles
[sw05492]
 proved and proof tools implemented. Builtin decision procedures and theorem provers can automatically establish...

CLAM
 Referenced in 28 articles
[sw19619]
 interactive proof editor into a fully automatic theorem proving system...

ETPS
 Referenced in 143 articles
[sw06302]
 used to prove theorems of first and higherorder logic interactively, automatically...

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

Epsilon
 Referenced in 35 articles
[sw00244]
 inequations, and handle and prove geometric theorems automatically...

ML
 Referenced in 458 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...

VAMPIRE
 Referenced in 186 articles
[sw02918]
 Vampire 8.0, [RV02,Vor05] is an automatic theorem prover for firstorder classical logic ... result to the kernel. When a theorem is proved, the system produces a verifiable proof...

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

TPS
 Referenced in 66 articles
[sw00973]
 used to prove theorems of first and higherorder logic interactively, automatically...

Zapato
 Referenced in 11 articles
[sw25425]
 zapato: Automatic theorem proving for predicate abstraction refinement. Counterexampledriven abstraction refinement is an automatic ... process is applied to software, an automatic theorem prover for quantifierfree firstorder logic...

MUSCADET
 Referenced in 9 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 pointset topology and topological linear spaces ... main ideas are exemplified by automatic proofs of some elementary facts on topological linear spaces...

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

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

HipSpec
 Referenced in 9 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 userstated properties. Experimental results are encouraging...

Electronic Geometry Textbook
 Referenced in 7 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...

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...

Juno2
 Referenced in 11 articles
[sw07216]
 been widely used in the automatic theoremproving community for the last two decades...

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

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

Analytica
 Referenced in 29 articles
[sw10478]
 Mathematica. Analytica is an automatic theorem prover for theorems in elementary analysis. The prover ... system to prove theorems that are beyond the scope of previous automatic theorem provers...