GeoCoq
From MaRDI portal
Software:43953
swMATH32242MaRDI QIDQ43953FDOQ43953
Author name not available (Why is that?)
Source code repository: https://github.com/GeoCoq/GeoCoq
Cited In (9)
- A synthetic proof of Pappus' theorem in Tarski's geometry
- Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
- 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
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- From Tarski to Hilbert
This page was built for software: GeoCoq
