GeoCoq

MaRDI QIDQ43953swMATHFDO

Official website https://geocoq.github.io/GeoCoq/

Source code repository https://github.com/GeoCoq/GeoCoq

Cited in

(13)

• Mechanical Theorem Proving in Tarski’s Geometry
• Complex_Geometry
• Poincare_Disc
• Formalization of the Poincaré disc model of hyperbolic geometry
• A synthetic proof of Pappus' theorem in Tarski's geometry
• Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq
• SerAPI
• GeoLogic
• 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 the universality of mathematical truth to the interoperability of proof systems
• From Tarski to Hilbert
• Proof-checking Euclid

This page was built for software: GeoCoq