GeoCoq

GeoCoq: A formalization of geometry in Coq based on Tarski’s axiom system. This library contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high-school.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 9 articles )

Showing results 1 to 9 of 9.
Sorted by year (citations)

  1. Simić, Danijela; Marić, Filip; Boutry, Pierre: Formalization of the Poincaré disc model of hyperbolic geometry (2021)
  2. Miroslav Olšák: GeoLogic - Graphical interactive theorem prover for Euclidean geometry (2020) arXiv
  3. Beeson, Michael; Narboux, Julien; Wiedijk, Freek: Proof-checking Euclid (2019)
  4. Boutry, Pierre; Braun, Gabriel; Narboux, Julien: Formalization of the arithmetization of Euclidean plane geometry and applications (2019)
  5. Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (2019)
  6. Braun, Gabriel; Narboux, Julien: A synthetic proof of Pappus’ theorem in Tarski’s geometry (2017)
  7. Stojanović Đurđević, Sana; Narboux, Julien; Janičić, Predrag: Automated generation of machine verifiable and readable proofs: a case study of Tarski’s geometry (2015)
  8. Braun, Gabriel; Narboux, Julien: From Tarski to Hilbert (2013)
  9. Narboux, Julien: Mechanical theorem proving in Tarski’s geometry (2007)