
MetiTarski
 Referenced in 49 articles
[sw00573]
 Many inequalities involving the functions ln, exp, sin...

ML
 Referenced in 514 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

VAMPIRE
 Referenced in 237 articles
[sw02918]
 Vampire 8.0, [RV02,Vor05] is an automatic theorem...

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

Metis_
 Referenced in 53 articles
[sw04439]
 Metis is an automatic theorem prover for first...

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

Mizar
 Referenced in 456 articles
[sw04704]
 The Mizar System is the only implementation of...

z3
 Referenced in 496 articles
[sw04887]
 Z3 is a highperformance theorem prover being...

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

MaLeCoP
 Referenced in 20 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 111 articles
[sw10277]
 Communicating formal proofs: the case of flyspeck. We...

MaLARea
 Referenced in 43 articles
[sw10278]
 MaLARea: a Metasystem for Automated Reasoning in Large...

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