- Referenced in 9 articles
- formalization of geometry in Coq based on Tarski’s axiom system. This library contains...
- Referenced in 2 articles
- 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...
- Referenced in 1880 articles
- Coq is a formal proof management system. It...
- Referenced in 698 articles
- Isabelle is a generic proof assistant. It allows...
- Referenced in 5363 articles
- The result of over 30 years of cutting...
- Referenced in 6337 articles
- Almost any workflow involves computing results, and that...
- Referenced in 522 articles
- ML (’Meta Language’) is a general-purpose functional...
- Referenced in 316 articles
- Our current automated deduction system Otter is designed...
- Referenced in 258 articles
- Vampire 8.0, [RV02,Vor05] is an automatic theorem...
- Referenced in 394 articles
- The TPTP (Thousands of Problems for Theorem Provers...
- Referenced in 144 articles
- Theorem proving system supporting both interactive proof development...
- Referenced in 505 articles
- The Mizar System is the only implementation of...
- Referenced in 197 articles
- Prover9 and Mace4: Prover9 is an automated theorem...
- Referenced in 12 articles
- A coherent logic based geometry theorem prover capable...
- Referenced in 160 articles
- PESCA = Proof Editor for Sequent Calculus: Pesca is...
- Referenced in 11 articles
- A synthesis of the procedural and declarative styles...