A case study in formalizing projective geometry in Coq: Desargues theorem
From MaRDI portal
Publication:448975
DOI10.1016/j.comgeo.2010.06.004zbMath1248.68449OpenAlexW2054653818MaRDI QIDQ448975
Pascal Schreck, Julien Narboux, Nicolas Magaud
Publication date: 11 September 2012
Published in: Computational Geometry (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.comgeo.2010.06.004
Related Items
A synthetic proof of Pappus' theorem in Tarski's geometry ⋮ Two cryptomorphic formalizations of projective incidence geometry ⋮ Duality notions in real projective plane ⋮ Formalizing Some “Small” Finite Models of Projective Geometry in Coq ⋮ Towards an intelligent and dynamic geometry book ⋮ The area method. A recapitulation ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry ⋮ Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry ⋮ An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs ⋮ Formalizing constructive projective geometry in Agda
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Non-Desarguian geometries and the foundations of geometry from David Hilbert to Ruth Moufang
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
- Formalizing Projective Plane Geometry in Coq
- DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY
- INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH
- Formalizing Hilbert’s Grundlagen in Isabelle/Isar
- Machine Proofs in Geometry
- Programming Languages and Systems
- Mechanical Theorem Proving in Tarski’s Geometry
- Theorem Proving in Higher Order Logics
This page was built for publication: A case study in formalizing projective geometry in Coq: Desargues theorem
