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
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Miroslav Olšák: GeoLogic - Graphical interactive theorem prover for Euclidean geometry (2020) arXiv
- Beeson, Michael; Narboux, Julien; Wiedijk, Freek: Proof-checking Euclid (2019)
- Boutry, Pierre; Braun, Gabriel; Narboux, Julien: Formalization of the arithmetization of Euclidean plane geometry and applications (2019)
- Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (2019)
- Braun, Gabriel; Narboux, Julien: A synthetic proof of Pappus’ theorem in Tarski’s geometry (2017)
- 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)
- Braun, Gabriel; Narboux, Julien: From Tarski to Hilbert (2013)
- Narboux, Julien: Mechanical theorem proving in Tarski’s geometry (2007)