A case study in formalizing projective geometry in Coq: Desargues theorem
From MaRDI portal
Publication:448975
DOI10.1016/J.COMGEO.2010.06.004zbMATH Open1248.68449OpenAlexW2054653818MaRDI QIDQ448975FDOQ448975
Authors: Nicolas Magaud, Julien Narboux, Pascal Schreck 
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
Recommendations
- Formalizing projective plane geometry in Coq
- Two cryptomorphic formalizations of projective incidence geometry
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq
- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
Cites Work
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Machine Proofs in Geometry
- DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY
- Mechanical Theorem Proving in Tarski’s Geometry
- Title not available (Why is that?)
- Non-Desarguian geometries and the foundations of geometry from David Hilbert to Ruth Moufang
- Title not available (Why is that?)
- Formalizing projective plane geometry in Coq
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Theorem Proving in Higher Order Logics
- 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
- INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH
- Title not available (Why is that?)
- Programming Languages and Systems
Cited In (17)
- A synthetic proof of Pappus' theorem in Tarski's geometry
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
- Formalization of the Poincaré disc model of hyperbolic geometry
- The area method. A recapitulation
- Theorem Proving in Higher Order Logics
- Two cryptomorphic formalizations of projective incidence geometry
- Formalizing projective plane geometry in Coq
- An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
- Duality notions in real projective plane
- Formalizing constructive projective geometry in Agda
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq
- Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach
- Two new ways to formally prove Dandelin-Gallucci's theorem
- Towards an intelligent and dynamic geometry book
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Some lemmas to hopefully enable search methods to find short and human readable proofs for incidence theorems of projective geometry
Uses Software
This page was built for publication: A case study in formalizing projective geometry in Coq: Desargues theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q448975)
