Formalizing projective plane geometry in Coq
From MaRDI portal
Publication:3003232
DOI10.1007/978-3-642-21046-4_7zbMATH Open1302.68246OpenAlexW1572941424MaRDI QIDQ3003232FDOQ3003232
Authors: Nicolas Magaud, Julien Narboux, Pascal Schreck 
Publication date: 26 May 2011
Published in: Automated Deduction in Geometry (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-21046-4_7
Recommendations
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq
- A case study in formalizing projective geometry in Coq: Desargues theorem
- Two cryptomorphic formalizations of projective incidence geometry
- Formalizing constructive projective geometry in Agda
- Formalization of the arithmetization of Euclidean plane geometry and applications
Cited In (19)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Combinatorial analysis of proofs in projective and affine geometry
- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
- The area method. A recapitulation
- A case study in formalizing projective geometry in Coq: Desargues theorem
- Theorem Proving in Higher Order Logics
- Two cryptomorphic formalizations of projective incidence geometry
- Formalization of the arithmetization of Euclidean plane geometry and applications
- Automated generation of geometric theorems from images of diagrams
- Formalizing complex plane geometry
- Duality notions in real projective plane
- A nonexistence certificate for projective planes of order ten with weight 15 codewords
- Title not available (Why is that?)
- Formalizing constructive projective geometry in Agda
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq
- A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Homography in \(\mathbb{R}\mathbb{P}^2\)
- Title not available (Why is that?)
Uses Software
This page was built for publication: Formalizing projective plane geometry in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3003232)
