
GeoCoq
 Referenced in 9 articles
[sw32242]
 formalization of geometry in Coq based on Tarski’s axiom system. This library contains...

Tarskis_Geometry
 Referenced in 2 articles
[sw32215]
 Tarski’s Euclidean axiom. Tarski’s axioms of plane geometry are formalized and, using ... shown to satisfy all of Tarski’s axioms except his Euclidean axiom ... thus Tarski’s Euclidean axiom is shown to be independent of his other axioms ... plane geometry. An earlier version of this work was the subject of the author...

Coq
 Referenced in 1880 articles
[sw00161]
 Coq is a formal proof management system. It...

Isabelle
 Referenced in 698 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

Maple
 Referenced in 5363 articles
[sw00545]
 The result of over 30 years of cutting...

Mathematica
 Referenced in 6337 articles
[sw00554]
 Almost any workflow involves computing results, and that...

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

OTTER
 Referenced in 316 articles
[sw02904]
 Our current automated deduction system Otter is designed...

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

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

Isar
 Referenced in 144 articles
[sw04599]
 Theorem proving system supporting both interactive proof development...

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

Prover9
 Referenced in 197 articles
[sw04969]
 Prover9 and Mace4: Prover9 is an automated theorem...

ArgoCLP
 Referenced in 12 articles
[sw07192]
 A coherent logic based geometry theorem prover capable...

Pesca
 Referenced in 160 articles
[sw13664]
 PESCA = Proof Editor for Sequent Calculus: Pesca is...

miz3
 Referenced in 11 articles
[sw18631]
 A synthesis of the procedural and declarative styles...