
HOL
 Referenced in 502 articles
[sw05492]
 Builtin decision procedures and theorem provers can automatically establish many simple theorems. An Oracle...

VAMPIRE
 Referenced in 237 articles
[sw02918]
 Vampire 8.0, [RV02,Vor05] is an automatic theorem prover for firstorder classical logic...

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

Sledgehammer
 Referenced in 119 articles
[sw07047]
 tool that harnesses external firstorder automatic theorem provers (ATPs) to discharge interactive proof obligations...

CVC4
 Referenced in 104 articles
[sw09485]
 CVC4 is an efficient opensource automatic theorem prover for satisfiability modulo theories (SMT) problems...

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

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

Analytica
 Referenced in 31 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 22 articles
[sw10186]
 SPIKE, an automatic theorem prover...

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

CeTA
 Referenced in 46 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 21 articles
[sw08206]
 Machine Learning for Sledgehammer. Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL...

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

AltErgo
 Referenced in 16 articles
[sw04888]
 Ergo is an automatic theorem prover dedicated to program verification. AltErgo is based...

Zapato
 Referenced in 11 articles
[sw25425]
 process is applied to software, an automatic theorem prover for quantifierfree firstorder logic ... report on a fast, lightweight, and automatic theorem prover called Zapato which we have built...

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

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

EMaLeS
 Referenced in 9 articles
[sw15190]
 important for the success of automatic theorem provers. EMaLeS is a metasystem that...

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