Cited in
(13)- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- A synthetic proof of Pappus' theorem in Tarski's geometry
- From the universality of mathematical truth to the interoperability of proof systems
- Proof-checking Euclid
- Formalization of the Poincaré disc model of hyperbolic geometry
- Mechanical Theorem Proving in Tarski’s Geometry
- Formalization of the arithmetization of Euclidean plane geometry and applications
- SerAPI
- GeoLogic
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- From Tarski to Hilbert
- Complex_Geometry
- Poincare_Disc
This page was built for software: GeoCoq
